# HG changeset patch
# User wenzelm
# Date 1717957193 -7200
# Node ID 94f3e6ff4576d0625b2986494288c3909a3c8404
# Parent  9aa11b457c3613660764f9ae6e31a8f8418be01f
clarified operations, including exceptions;

diff -r 9aa11b457c36 -r 94f3e6ff4576 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Jun 09 20:04:41 2024 +0200
+++ b/src/Pure/Isar/element.ML	Sun Jun 09 20:19:53 2024 +0200
@@ -226,11 +226,12 @@
 
 fun thm_name ctxt kind th prts =
   let val head =
-    if Thm.has_name_hint th then
-      Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
-        Thy_Header.pretty_name' ctxt (Long_Name.base_name (#1 (Thm.get_name_hint th))),
-        Pretty.str ":"]
-    else Pretty.keyword1 kind
+    (case try Thm.the_name_hint th of
+      SOME (name, _) =>
+        Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
+          Thy_Header.pretty_name' ctxt (Long_Name.base_name name),
+          Pretty.str ":"]
+    | NONE => Pretty.keyword1 kind)
   in Pretty.block (Pretty.fbreaks (head :: prts)) end;
 
 fun obtain prop ctxt =
diff -r 9aa11b457c36 -r 94f3e6ff4576 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Jun 09 20:04:41 2024 +0200
+++ b/src/Pure/more_thm.ML	Sun Jun 09 20:19:53 2024 +0200
@@ -87,6 +87,7 @@
   val def_binding: Binding.binding -> Binding.binding
   val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
   val make_def_binding: bool -> Binding.binding -> Binding.binding
+  val the_name_hint: thm -> Thm_Name.T  (*exception THM*)
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> Thm_Name.T
   val put_name_hint: Thm_Name.T -> thm -> thm
@@ -606,9 +607,16 @@
 
 (* unofficial theorem names *)
 
-fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN;
-fun the_name_hint thm = Thm_Name.parse (the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN));
-fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else ("??.unknown", 0);
+fun the_name_hint thm =
+  let val thm_name = Thm_Name.parse (Properties.get_string (Thm.get_tags thm) Markup.nameN)
+  in
+    if Thm_Name.is_empty thm_name
+    then raise THM ("Thm.the_name_hint: missing name", 0, [thm])
+    else thm_name
+  end;
+
+fun has_name_hint thm = can the_name_hint thm;
+fun get_name_hint thm = try the_name_hint thm |> the_default ("??.unknown", 0);
 
 fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, Thm_Name.print name);