tuned signature;

--- a/src/Pure/thm.ML	Fri Jun 07 12:39:14 2024 +0200
+++ b/src/Pure/thm.ML	Fri Jun 07 13:19:39 2024 +0200
@@ -176,8 +176,8 @@
   val plain_prop_of: thm -> term
   val get_zproof_serials: theory -> serial list
   val get_zproof: theory -> serial ->
-    {name: Thm_Name.T * Position.T, thm: thm, zboxes: ZTerm.zboxes, zproof: zproof} option
-  val store_zproof: Thm_Name.T * Position.T -> thm -> theory -> thm * theory
+    {name: Thm_Name.P, thm: thm, zboxes: ZTerm.zboxes, zproof: zproof} option
+  val store_zproof: Thm_Name.P -> thm -> theory -> thm * theory
   val dest_state: thm * int -> (term * term) list * term list * term * term
   val lift_rule: cterm -> thm -> thm
   val incr_indexes: int -> thm -> thm
@@ -951,7 +951,7 @@
 structure Data = Theory_Data
 (
   type T =
-    {name: Thm_Name.T * Position.T, thm: thm} Inttab.table *  (*stored zproof thms*)
+    {name: Thm_Name.P, thm: thm} Inttab.table *  (*stored zproof thms*)
     unit Name_Space.table *  (*oracles: authentic derivation names*)
     classes;  (*type classes within the logic*)
 

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

--- a/src/Pure/zterm.ML	Fri Jun 07 12:39:14 2024 +0200
+++ b/src/Pure/zterm.ML	Fri Jun 07 13:19:39 2024 +0200
@@ -195,7 +195,7 @@
 datatype zproof_name =
     ZAxiom of string
   | ZOracle of string
-  | ZThm of {theory_name: string, thm_name: Thm_Name.T * Position.T, serial: serial};
+  | ZThm of {theory_name: string, thm_name: Thm_Name.P, serial: serial};
 
 type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table);
 
@@ -274,7 +274,7 @@
   val unions_zboxes: zboxes list -> zboxes
   val add_box_proof: {unconstrain: bool} -> theory ->
     term list -> term -> zproof -> zboxes -> zproof * zboxes
-  val thm_proof: theory -> Thm_Name.T * Position.T -> term list -> term -> zproof -> zbox * zproof
+  val thm_proof: theory -> Thm_Name.P -> term list -> term -> zproof -> zbox * zproof
   val axiom_proof:  theory -> string -> term -> zproof
   val oracle_proof:  theory -> string -> term -> zproof
   val assume_proof: theory -> term -> zproof