# HG changeset patch
# User wenzelm
# Date 1734289965 -3600
# Node ID af21a61dadada78ae784a203cc6035e37637c289
# Parent  ed264056f5dc875d156d808b8a399d9f68a44d98
clarified signature (see also 2157039256d3);

diff -r ed264056f5dc -r af21a61dadad src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Dec 15 14:59:57 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Dec 15 20:12:45 2024 +0100
@@ -407,7 +407,7 @@
 fun extern_fixed ctxt x = if Name.is_skolem x then Variable.revert_fixed ctxt x else x;
 
 fun extern_entity ctxt =
-  Lexicon.unmark
+  Lexicon.unmark_entity
    {case_class = extern_class ctxt,
     case_type = extern_type ctxt,
     case_const = extern_const ctxt,
diff -r ed264056f5dc -r af21a61dadad src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Dec 15 14:59:57 2024 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sun Dec 15 20:12:45 2024 +0100
@@ -67,13 +67,13 @@
   val mark_type: string -> string val unmark_type: string -> string val is_type: string -> bool
   val mark_const: string -> string val unmark_const: string -> string val is_const: string -> bool
   val mark_fixed: string -> string val unmark_fixed: string -> string val is_fixed: string -> bool
-  val unmark:
+  val unmark_entity:
    {case_class: string -> 'a,
     case_type: string -> 'a,
     case_const: string -> 'a,
     case_fixed: string -> 'a,
     case_default: string -> 'a} -> string -> 'a
-  val is_marked: string -> bool
+  val is_marked_entity: string -> bool
   val dummy_type: term
   val fun_type: term
 end;
@@ -497,7 +497,7 @@
 val (mark_const, unmark_const, is_const) = marker "\<^const>";
 val (mark_fixed, unmark_fixed, is_fixed) = marker "\<^fixed>";
 
-fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
+fun unmark_entity {case_class, case_type, case_const, case_fixed, case_default} s =
   (case try unmark_class s of
     SOME c => case_class c
   | NONE =>
@@ -511,8 +511,8 @@
                 SOME c => case_fixed c
               | NONE => case_default s))));
 
-val is_marked =
-  unmark {case_class = K true, case_type = K true, case_const = K true,
+val is_marked_entity =
+  unmark_entity {case_class = K true, case_type = K true, case_const = K true,
     case_fixed = K true, case_default = K false};
 
 val dummy_type = Syntax.const (mark_type "dummy");
diff -r ed264056f5dc -r af21a61dadad src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Dec 15 14:59:57 2024 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sun Dec 15 20:12:45 2024 +0100
@@ -498,7 +498,7 @@
       |> Option.map Prefix);
 
 fun is_const (Syntax ({consts, ...}, _)) c =
-  Graph.defined consts c andalso not (Lexicon.is_marked c);
+  Graph.defined consts c andalso not (Lexicon.is_marked_entity c);
 
 fun is_keyword (Syntax ({keywords, ...}, _)) = member_keywords keywords;
 fun tokenize (Syntax ({keywords, ...}, _)) = tokenize_keywords keywords;
@@ -538,7 +538,7 @@
   else [c];
 
 fun add_consts (c, bs) consts =
-  if c = "" orelse (null bs andalso (Lexicon.is_marked c orelse Graph.defined consts c))
+  if c = "" orelse (null bs andalso (Lexicon.is_marked_entity c orelse Graph.defined consts c))
   then consts
   else
     consts
diff -r ed264056f5dc -r af21a61dadad src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Dec 15 14:59:57 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Dec 15 20:12:45 2024 +0100
@@ -66,7 +66,7 @@
 
 fun markup_entity ctxt c =
   Syntax.get_consts (Proof_Context.syntax_of ctxt) c
-  |> maps (Lexicon.unmark
+  |> maps (Lexicon.unmark_entity
      {case_class = markup_class ctxt,
       case_type = markup_type ctxt,
       case_const = markup_const ctxt,
@@ -722,7 +722,7 @@
   (case Syntax.get_consts (Proof_Context.syntax_of ctxt) c of
     [b] => b
   | bs =>
-      (case filter Lexicon.is_marked bs of
+      (case filter Lexicon.is_marked_entity bs of
         [] => c
       | [b] => b
       | _ => error ("Multiple logical entities for " ^ quote c ^ ": " ^ commas_quote bs)))
diff -r ed264056f5dc -r af21a61dadad src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Dec 15 14:59:57 2024 +0100
+++ b/src/Pure/sign.ML	Sun Dec 15 20:12:45 2024 +0100
@@ -527,7 +527,7 @@
     fun print_type c = uncurry Markup.markup (Name_Space.markup_extern ctxt (type_space thy) c);
     fun print_const c = uncurry Markup.markup (Name_Space.markup_extern ctxt (const_space thy) c);
   in
-    s |> Lexicon.unmark
+    s |> Lexicon.unmark_entity
      {case_class = K (),
       case_type = fn c =>
         if declared_tyname thy c then () else error ("Not a global type: " ^ quote (print_type c)),