diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index ec6448f56fcd..33e9a241e604 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/src/Lean/Elab/InfoTree/Main.lean
@@ -26,6 +26,27 @@ def save [MonadFileMap m] : m CommandContextInfo := do
 
 end CommandContextInfo
 
+/--
+Merges the `inner` partial context into the `outer` context s.t. fields of the `inner` context
+overwrite fields of the `outer` context. Panics if the invariant described in the documentation
+for `PartialContextInfo` is violated.
+
+When traversing an `InfoTree`, this function should be used to combine the context of outer
+nodes with the partial context of their subtrees. This ensures that the traversal has the context
+from the inner node to the root node of the `InfoTree` available, with partial contexts of
+inner nodes taking priority over contexts of outer nodes.
+-/
+def PartialContextInfo.mergeIntoOuter?
+    : (inner : PartialContextInfo) → (outer? : Option ContextInfo) → Option ContextInfo
+  | .commandCtx info, none =>
+    some { info with }
+  | .parentDeclCtx _, none =>
+    panic! "Unexpected incomplete InfoTree context info."
+  | .commandCtx innerInfo, some outer =>
+    some { outer with toCommandContextInfo := innerInfo }
+  | .parentDeclCtx innerParentDecl, some outer =>
+    some { outer with parentDecl? := innerParentDecl }
+
 def CompletionInfo.stx : CompletionInfo → Syntax
   | dot i .. => i.stx
   | id stx .. => stx
diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean
index ed93c69fd040..2fd90e69b260 100644
--- a/src/Lean/Elab/InfoTree/Types.lean
+++ b/src/Lean/Elab/InfoTree/Types.lean
@@ -46,27 +46,6 @@ inductive PartialContextInfo where
   -- TODO: More constructors for the different kinds of scopes `commandCtx` is currently
   -- used for (e.g. eliminating `Info.updateContext?` would be nice!).
 
-/--
-Merges the `inner` partial context into the `outer` context s.t. fields of the `inner` context
-overwrite fields of the `outer` context. Panics if the invariant described in the documentation
-for `PartialContextInfo` is violated.
-
-When traversing an `InfoTree`, this function should be used to combine the context of outer
-nodes with the partial context of their subtrees. This ensures that the traversal has the context
-from the inner node to the root node of the `InfoTree` available, with partial contexts of
-inner nodes taking priority over contexts of outer nodes.
--/
-def PartialContextInfo.mergeIntoOuter?
-    : (inner : PartialContextInfo) → (outer? : Option ContextInfo) → Option ContextInfo
-  | .commandCtx info, none =>
-    some { info with }
-  | .parentDeclCtx _, none =>
-    panic! "Unexpected incomplete InfoTree context info."
-  | .commandCtx innerInfo, some outer =>
-    some { outer with toCommandContextInfo := innerInfo }
-  | .parentDeclCtx innerParentDecl, some outer =>
-    some { outer with parentDecl? := innerParentDecl }
-
 /-- Base structure for `TermInfo`, `CommandInfo` and `TacticInfo`. -/
 structure ElabInfo where
   /-- The name of the elaborator that created this info. -/