--- 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);