src/Pure/thm_name.ML

--- a/src/Pure/thm_name.ML	Fri Jun 07 12:39:14 2024 +0200
+++ b/src/Pure/thm_name.ML	Fri Jun 07 13:19:39 2024 +0200
@@ -11,11 +11,12 @@
 sig
   type T = string * int
   val ord: T ord
-  val none: T * Position.T
+  type P = T * Position.T
+  val none: P
   val print: T -> string
-  val short: T * Position.T -> string * Position.T
-  val list: string * Position.T -> 'a list -> ((T * Position.T) * 'a) list
-  val expr: string * Position.T -> ('a list * 'b) list -> (((T * Position.T) * 'a) list * 'b) list
+  val short: P -> string * Position.T
+  val list: string * Position.T -> 'a list -> (P * 'a) list
+  val expr: string * Position.T -> ('a list * 'b) list -> ((P * 'a) list * 'b) list
 end;
 
 structure Thm_Name: THM_NAME =
@@ -24,17 +25,19 @@
 type T = string * int;
 val ord = prod_ord string_ord int_ord;
 
-val none = (("", 0), Position.none);
+type P = T * Position.T;
+
+val none: P = (("", 0), Position.none);
 
 fun print (name, index) =
   if name = "" orelse index = 0 then name
   else name ^ enclose "(" ")" (string_of_int index);
 
-fun short ((name, index), pos: Position.T) =
+fun short (((name, index), pos): P) =
   if name = "" orelse index = 0 then (name, pos)
   else (name ^ "_" ^ string_of_int index, pos);
 
-fun list (name, pos: Position.T) [thm] = [(((name, 0): T, pos), thm)]
+fun list (name, pos) [thm] = [(((name, 0), pos): P, thm)]
   | list (name, pos) thms = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) thms;
 
 fun expr name = burrow_fst (burrow (list name));