diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
index d7bcb1b..f3442da 100644
--- a/DocGen4/Process/Base.lean
+++ b/DocGen4/Process/Base.lean
@@ -166,7 +166,7 @@ inductive DocInfo where
 Turns an `Expr` into a pretty printed `CodeWithInfos`.
 -/
 def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
-  let (fmt, infos) ←  PrettyPrinter.ppExprWithInfos expr
+  let ⟨fmt, infos⟩ ←  PrettyPrinter.ppExprWithInfos expr
   let tt := TaggedText.prettyTagged fmt
   let ctx := {
     env := ← getEnv
@@ -177,7 +177,7 @@ def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
     fileMap := default,
     ngen := ← getNGen
   }
-  pure <| tagExprInfos ctx infos tt
+  pure <| tagCodeInfos ctx infos tt
 
 def isInstance (declName : Name) : MetaM Bool := do
   pure <| (instanceExtension.getState (←getEnv)).instanceNames.contains declName
diff --git a/lake-manifest.json b/lake-manifest.json
index c8fda0d..25d183b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -22,7 +22,7 @@
   {"git":
    {"url": "https://github.com/hargonix/LeanInk",
     "subDir?": null,
-    "rev": "9f3101452135964ac9107ec8e9910bfd14022bbc",
+    "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
     "name": "leanInk",
     "inputRev?": "doc-gen"}},
   {"git":
diff --git a/lean-toolchain b/lean-toolchain
index a01662b..ca5c312 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-12-05
+leanprover/lean4:nightly-2022-12-16