# HG changeset patch
# User wenzelm
# Date 1733144908 -3600
# Node ID d230683a35fc615a674d0785a1c2ca7f5a54e89c
# Parent  aed257e030d235120706f114f4e1dcc96727ec2b
more direct Proof_Context.lookup_free -- bypass redundancy of Proof_Context.check_const;

diff -r aed257e030d2 -r d230683a35fc src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Dec 02 11:45:42 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Dec 02 14:08:28 2024 +0100
@@ -42,6 +42,7 @@
   val class_space: Proof.context -> Name_Space.T
   val type_space: Proof.context -> Name_Space.T
   val const_space: Proof.context -> Name_Space.T
+  val lookup_free: Proof.context -> string -> string option
   val defs_context: Proof.context -> Defs.context
   val intern_class: Proof.context -> xstring -> string
   val intern_type: Proof.context -> xstring -> string
@@ -351,11 +352,30 @@
 val concealed = map_naming Name_Space.concealed;
 
 
+(* const vs. free *)
+
+val const_space = Consts.space_of o consts_of;
+
+fun is_const_declared ctxt x =
+  let val space = const_space ctxt
+  in Name_Space.declared space (Name_Space.intern space x) end;
+
+fun lookup_free ctxt x =
+  if Variable.is_const ctxt x then NONE
+  else
+    (case Variable.lookup_fixed ctxt x of
+      NONE =>
+        let
+          val is_const = Long_Name.is_qualified x orelse is_const_declared ctxt x;
+          val is_free_declared = is_some (Variable.default_type ctxt x);
+        in if not is_const orelse is_free_declared then SOME x else NONE end
+    | fixed => fixed);
+
+
 (* name spaces *)
 
 val class_space = Type.class_space o tsig_of;
 val type_space = Type.type_space o tsig_of;
-val const_space = Consts.space_of o consts_of;
 
 fun defs_context ctxt = (ctxt, (const_space ctxt, type_space ctxt));
 
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 **)