# HG changeset patch
# User wenzelm
# Date 1733146210 -3600
# Node ID 69defb70caf74e29dc2f0a7d801b5b04d851cd75
# Parent  d230683a35fc615a674d0785a1c2ca7f5a54e89c
more accurate extern_const: avoid clash with frees;

diff -r d230683a35fc -r 69defb70caf7 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Dec 02 14:08:28 2024 +0100
+++ b/src/Pure/General/name_space.ML	Mon Dec 02 14:30:10 2024 +0100
@@ -28,6 +28,7 @@
   val names_long: bool Config.T
   val names_short: bool Config.T
   val names_unique: bool Config.T
+  val extern_if: (xstring -> bool) -> Proof.context -> T -> string -> xstring
   val extern: Proof.context -> T -> string -> xstring
   val extern_ord: Proof.context -> T -> string ord
   val extern_shortest: Proof.context -> T -> string -> xstring
@@ -291,7 +292,7 @@
 val names_short = Config.declare_option_bool ("names_short", \<^here>);
 val names_unique = Config.declare_option_bool ("names_unique", \<^here>);
 
-fun extern ctxt space name =
+fun extern_if ok ctxt space name =
   let
     val names_long = Config.get ctxt names_long;
     val names_short = Config.get ctxt names_short;
@@ -299,8 +300,9 @@
 
     fun extern_chunks require_unique a chunks =
       let val {full_name = c, unique, ...} = intern_chunks space chunks in
-        if (not require_unique orelse unique) andalso is_alias space c a
-        then SOME (Long_Name.implode_chunks chunks)
+        if (not require_unique orelse unique) andalso is_alias space c a then
+          let val x = Long_Name.implode_chunks chunks
+          in if ok x then SOME x else NONE end
         else NONE
       end;
 
@@ -321,6 +323,8 @@
     else extern_names (get_aliases space name)
   end;
 
+val extern = extern_if (K true);
+
 fun extern_ord ctxt space = string_ord o apply2 (extern ctxt space);
 
 fun extern_shortest ctxt =
diff -r d230683a35fc -r 69defb70caf7 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Dec 02 14:08:28 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Dec 02 14:30:10 2024 +0100
@@ -385,7 +385,7 @@
 
 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 ctxt (const_space ctxt);
+fun extern_const ctxt = Name_Space.extern_if (is_none o lookup_free ctxt) ctxt (const_space ctxt);
 
 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;