diff -r 360e6217cda6 -r 00d68f324056 src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Thu Jun 06 23:19:59 2024 +0200
+++ b/src/Pure/thm_name.ML	Fri Jun 07 11:10:49 2024 +0200
@@ -11,6 +11,7 @@
 sig
   type T = string * int
   val ord: T ord
+  val none: T * Position.T
   val print: T -> string
   val short: T * Position.T -> string * Position.T
   val list: string * Position.T -> 'a list -> ((T * Position.T) * 'a) list
@@ -23,6 +24,8 @@
 type T = string * int;
 val ord = prod_ord string_ord int_ord;
 
+val none = (("", 0), Position.none);
+
 fun print (name, index) =
   if name = "" orelse index = 0 then name
   else name ^ enclose "(" ")" (string_of_int index);