# HG changeset patch
# User wenzelm
# Date 1717751449 -7200
# Node ID 00d68f3240567334f406aa459b9a32b608c5060c
# Parent  360e6217cda61d8c76455195ccc281fb84b9c9cb
tuned signature: just one ZThm is sufficient;

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);
diff -r 360e6217cda6 -r 00d68f324056 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jun 06 23:19:59 2024 +0200
+++ b/src/Pure/zterm.ML	Fri Jun 07 11:10:49 2024 +0200
@@ -195,7 +195,6 @@
 datatype zproof_name =
     ZAxiom of string
   | ZOracle of string
-  | ZBox of {theory_name: string, serial: serial}
   | ZThm of {theory_name: string, thm_name: Thm_Name.T * Position.T, serial: serial};
 
 type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table);
@@ -857,7 +856,7 @@
       | proof _ _ = raise Same.SAME;
   in ZAbsps prems (Same.commit (proof 0) prf) end;
 
-fun box_proof {unconstrain} zproof_name thy hyps concl prf =
+fun box_proof {unconstrain} thy thm_name hyps concl prf =
   let
     val {zterm, ...} = zterm_cache thy;
 
@@ -898,7 +897,10 @@
     val i = serial ();
     val zbox: zbox = (i, (prop', prf'));
 
-    val const = constrain_proof (ZConstp (zproof_const (zproof_name i, prop')));
+    val proof_name =
+      ZThm {theory_name = Context.theory_long_name thy, thm_name = thm_name, serial = i};
+
+    val const = constrain_proof (ZConstp (zproof_const (proof_name, prop')));
     val args1 =
       outer_constraints |> map (fn (T, c) =>
         ZClassp (ztyp_of (if unconstrain then unconstrain_typ T else T), c));
@@ -907,17 +909,11 @@
 
 in
 
-fun thm_proof thy thm_name =
-  let
-    val thy_name = Context.theory_long_name thy;
-    fun zproof_name i = ZThm {theory_name = thy_name, thm_name = thm_name, serial = i};
-  in box_proof {unconstrain = false} zproof_name thy end;
+val thm_proof = box_proof {unconstrain = false};
 
 fun add_box_proof unconstrain thy hyps concl prf zboxes =
   let
-    val thy_name = Context.theory_long_name thy;
-    fun zproof_name i = ZBox {theory_name = thy_name, serial = i};
-    val (zbox, prf') = box_proof unconstrain zproof_name thy hyps concl prf;
+    val (zbox, prf') = box_proof unconstrain thy Thm_Name.none hyps concl prf;
     val zboxes' = add_zboxes zbox zboxes;
   in (prf', zboxes') end;