diff -r aed257e030d2 -r d230683a35fc src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Dec 02 11:45:42 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Dec 02 14:08:28 2024 +0100
@@ -265,22 +265,6 @@
   Proof_Context.check_const {proper = true, strict = false} ctxt (c, ps)
   |>> dest_Const_name;
 
-local
-
-fun get_free ctxt x =
-  let
-    val fixed = Variable.lookup_fixed ctxt x;
-    val is_const = can (decode_const ctxt) (x, []) orelse Long_Name.is_qualified x;
-    val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
-  in
-    if Variable.is_const ctxt x then NONE
-    else if is_some fixed then fixed
-    else if not is_const orelse is_declared then SOME x
-    else NONE
-  end;
-
-in
-
 fun decode_term ctxt =
   let
     val markup_free_cache = #apply (Symtab.unsynchronized_cache (markup_free ctxt));
@@ -319,7 +303,7 @@
               | decode ps _ _ (Free (a, T)) =
                   ((Name.reject_internal (a, ps) handle ERROR msg =>
                       error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
-                    (case get_free ctxt a of
+                    (case Proof_Context.lookup_free ctxt a of
                       SOME x => (report ps markup_free_cache x; Free (x, T))
                     | NONE =>
                         let
@@ -337,8 +321,6 @@
 
   in decode end;
 
-end;
-
 
 
 (** parse **)