--- 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 **)