# HG changeset patch
# User wenzelm
# Date 1733162025 -3600
# Node ID 8e4ca2c87e86476ca18c564eb3535accb8600157
# Parent  69defb70caf74e29dc2f0a7d801b5b04d851cd75
clarified modules;

diff -r 69defb70caf7 -r 8e4ca2c87e86 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Dec 02 14:30:10 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Dec 02 18:53:45 2024 +0100
@@ -54,6 +54,8 @@
   val markup_type: Proof.context -> string -> string
   val pretty_type: Proof.context -> string -> Pretty.T
   val extern_const: Proof.context -> string -> xstring
+  val extern_fixed: Proof.context -> string -> string
+  val extern_entity: Proof.context -> string -> string
   val markup_const: Proof.context -> string -> string
   val pretty_const: Proof.context -> string -> Pretty.T
   val transfer: theory -> Proof.context -> Proof.context
@@ -386,6 +388,15 @@
 fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt);
 fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt);
 fun extern_const ctxt = Name_Space.extern_if (is_none o lookup_free ctxt) ctxt (const_space ctxt);
+fun extern_fixed ctxt x = if Name.is_skolem x then Variable.revert_fixed ctxt x else x;
+
+fun extern_entity ctxt =
+  Lexicon.unmark
+   {case_class = extern_class ctxt,
+    case_type = extern_type ctxt,
+    case_const = extern_const ctxt,
+    case_fixed = extern_fixed ctxt,
+    case_default = I};
 
 fun markup_class ctxt c = Name_Space.markup_extern ctxt (class_space ctxt) c |-> Markup.markup;
 fun markup_type ctxt c = Name_Space.markup_extern ctxt (type_space ctxt) c |-> Markup.markup;
diff -r 69defb70caf7 -r 8e4ca2c87e86 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Dec 02 14:30:10 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Dec 02 18:53:45 2024 +0100
@@ -713,9 +713,6 @@
 
 local
 
-fun extern_fixed ctxt x =
-  if Name.is_skolem x then Variable.revert_fixed ctxt x else x;
-
 fun extern_cache ctxt =
   Symtab.unsynchronized_cache (fn c =>
     (case Syntax.get_consts (Proof_Context.syntax_of ctxt) c of
@@ -725,12 +722,7 @@
           [] => c
         | [b] => b
         | _ => error ("Multiple logical entities for " ^ quote c ^ ": " ^ commas_quote bs)))
-    |> Lexicon.unmark
-       {case_class = Proof_Context.extern_class ctxt,
-        case_type = Proof_Context.extern_type ctxt,
-        case_const = Proof_Context.extern_const ctxt,
-        case_fixed = extern_fixed ctxt,
-        case_default = I})
+    |> Proof_Context.extern_entity ctxt)
   |> #apply;
 
 val var_or_skolem_cache =
@@ -759,7 +751,8 @@
     val extern = extern_cache ctxt;
 
     val free_or_skolem_cache =
-      #apply (Symtab.unsynchronized_cache (fn x => (markup_free ctxt x, extern_fixed ctxt x)));
+      Symtab.unsynchronized_cache (fn x => (markup_free ctxt x, Proof_Context.extern_fixed ctxt x))
+      |> #apply;
 
     val cache1 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table);
     val cache2 = Unsynchronized.ref (Ast.Table.empty: Markup.output Pretty.block Ast.Table.table);