# HG changeset patch
# User wenzelm
# Date 1703188982 -3600
# Node ID 992c494bda25a8d91979f1570cffecaee937eb16
# Parent  1cdc1a3acdcd96530ca09aeadfc046a9698483fb
proper thm_name for stored zproof;

diff -r 1cdc1a3acdcd -r 992c494bda25 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Dec 21 17:07:03 2023 +0100
+++ b/src/Pure/ROOT.ML	Thu Dec 21 21:03:02 2023 +0100
@@ -176,6 +176,7 @@
 ML_file "theory.ML";
 ML_file "term_sharing.ML";
 ML_file "term_xml.ML";
+ML_file "thm_name.ML";
 ML_file "zterm.ML";
 ML_file "proofterm.ML";
 ML_file "thm.ML";
@@ -185,7 +186,6 @@
 ML_file "more_thm.ML";
 
 ML_file "facts.ML";
-ML_file "thm_name.ML";
 ML_file "global_theory.ML";
 ML_file "pure_thy.ML";
 ML_file "drule.ML";
diff -r 1cdc1a3acdcd -r 992c494bda25 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Thu Dec 21 17:07:03 2023 +0100
+++ b/src/Pure/global_theory.ML	Thu Dec 21 21:03:02 2023 +0100
@@ -249,15 +249,18 @@
   if Proofterm.any_proofs_enabled () orelse Options.default_bool "strict_facts"
   then Lazy.force_value thms else thms;
 
-fun register_proofs_lazy thms thy =
+fun register_proofs_lazy (name, pos) (thms: thm list Lazy.lazy) thy =
   let
     val (thms', thy') =
-      if Proofterm.zproof_enabled (Proofterm.get_proofs_level ())
-      then fold_map Thm.store_zproof (Lazy.force thms) thy |>> Lazy.value
+      if name <> "" andalso Proofterm.zproof_enabled (Proofterm.get_proofs_level ()) then
+        fold_map (fn (a, th) => Thm.store_zproof (a, pos) th)
+          (Thm_Name.make_list name (Lazy.force thms)) thy
+        |>> Lazy.value
       else (check_thms_lazy thms, thy);
   in (thms', Thm.register_proofs thms' thy') end;
 
-fun register_proofs thms = register_proofs_lazy (Lazy.value thms) #>> Lazy.force;
+fun register_proofs name thms =
+  register_proofs_lazy name (Lazy.value thms) #>> Lazy.force;
 
 
 fun bind_name thy b = (Sign.full_name thy b, Binding.default_pos_of b);
@@ -290,13 +293,13 @@
   end;
 
 fun add_thms_lazy kind (b, thms) thy =
-  if Binding.is_empty b then register_proofs_lazy thms thy |> #2
-  else
-    let
-      val name_pos = bind_name thy b;
-      val thms' = thms
-        |> Lazy.map_finished (name_thms official1 name_pos #> map (Thm.kind_rule kind));
-    in thy |> register_proofs_lazy thms' |-> curry add_facts b end;
+  let val (name, pos) = bind_name thy b in
+    if name = "" then register_proofs_lazy (name, pos) thms thy |> #2
+    else
+      register_proofs_lazy (name, pos)
+        (Lazy.map_finished (name_thms official1 (name, pos) #> map (Thm.kind_rule kind)) thms) thy
+      |-> curry add_facts b
+  end;
 
 
 (* apply theorems and attributes *)
@@ -310,15 +313,17 @@
 in
 
 fun apply_facts name_flags1 name_flags2 (b, facts) thy =
-  if Binding.is_empty b then app_facts facts thy |-> register_proofs
-  else
-    let
-      val name_pos = bind_name thy b;
-      val (thms', thy') = thy
-        |> app_facts (map (apfst (name_thms name_flags1 name_pos)) facts)
-        |>> name_thms name_flags2 name_pos |-> register_proofs;
-      val thy'' = thy' |> add_facts (b, Lazy.value thms');
-    in (map (Thm.transfer thy'') thms', thy'') end;
+  let val (name, pos) = bind_name thy b in
+    if name = "" then app_facts facts thy |-> register_proofs (name, pos)
+    else
+      let
+        val name_pos = bind_name thy b;
+        val (thms', thy') = thy
+          |> app_facts (map (apfst (name_thms name_flags1 name_pos)) facts)
+          |>> name_thms name_flags2 name_pos |-> register_proofs (name, pos);
+        val thy'' = thy' |> add_facts (b, Lazy.value thms');
+      in (map (Thm.transfer thy'') thms', thy'') end
+  end;
 
 end;
 
diff -r 1cdc1a3acdcd -r 992c494bda25 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Dec 21 17:07:03 2023 +0100
+++ b/src/Pure/thm.ML	Thu Dec 21 21:03:02 2023 +0100
@@ -174,7 +174,7 @@
   val legacy_freezeT: thm -> thm
   val plain_prop_of: thm -> term
   val get_zproof: theory -> serial -> {prop: zterm, zboxes: ZTerm.zboxes, zproof: zproof} option
-  val store_zproof: thm -> theory -> thm * theory
+  val store_zproof: Thm_Name.T * Position.T -> 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
@@ -2074,14 +2074,14 @@
 
 val get_zproof = Inttab.lookup o get_zproofs;
 
-fun store_zproof thm thy =
+fun store_zproof name thm thy =
   let
     val Thm (Deriv {promises, body = PBody body}, args as {hyps, prop, ...}) = thm;
     val {oracles, thms, zboxes, zproof, proof} = body;
     val _ = null promises orelse
       raise THM ("store_zproof: theorem may not use promises", 0, [thm]);
 
-    val ((i, (zprop, zprf)), zproof') = ZTerm.thm_proof thy hyps prop zproof;
+    val ((i, (zprop, zprf)), zproof') = ZTerm.thm_proof thy name hyps prop zproof;
     val thy' = thy
       |> map_zproofs (Inttab.update (i, {prop = zprop, zboxes = zboxes, zproof = zprf}));
     val der' = make_deriv promises oracles thms [] zproof' proof;
diff -r 1cdc1a3acdcd -r 992c494bda25 src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Thu Dec 21 17:07:03 2023 +0100
+++ b/src/Pure/thm_name.ML	Thu Dec 21 21:03:02 2023 +0100
@@ -13,7 +13,7 @@
   val ord: T ord
   val print: T -> string
   val flatten: T -> string
-  val make_list: string -> thm list -> (T * thm) list
+  val make_list: string -> 'a list -> (T * 'a) list
 end;
 
 structure Thm_Name: THM_NAME =
@@ -30,7 +30,7 @@
   if name = "" orelse index = 0 then name
   else name ^ "_" ^ string_of_int index;
 
-fun make_list name [thm: thm] = [((name, 0), thm)]
+fun make_list name [thm] = [((name, 0), thm)]
   | make_list name thms = map_index (fn (i, thm) => ((name, i + 1), thm)) thms;
 
 end;
diff -r 1cdc1a3acdcd -r 992c494bda25 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Dec 21 17:07:03 2023 +0100
+++ b/src/Pure/zterm.ML	Thu Dec 21 21:03:02 2023 +0100
@@ -198,7 +198,7 @@
     ZAxiom of string
   | ZOracle of string
   | ZBox of serial
-  | ZThm of serial;
+  | ZThm of {theory_long_name: string, thm_name: Thm_Name.T, pos: Position.T, serial: int};
 
 datatype zproof =
     ZDummy                         (*dummy proof*)
@@ -267,7 +267,7 @@
   val union_zboxes: zboxes -> zboxes -> zboxes
   val unions_zboxes: zboxes list -> zboxes
   val add_box_proof: theory -> term list -> term -> zboxes * zproof -> zboxes * zproof
-  val thm_proof: theory -> term list -> term -> zproof -> zbox * zproof
+  val thm_proof: theory -> Thm_Name.T * Position.T -> 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
@@ -817,7 +817,12 @@
 
 in
 
-val thm_proof = box_proof ZThm;
+fun thm_proof thy (name, pos) =
+  let
+    val thy_name = Context.theory_long_name thy;
+    fun zproof_name i =
+      ZThm {theory_long_name = thy_name, thm_name = name, pos = pos, serial = i};
+  in box_proof zproof_name thy end;
 
 fun add_box_proof thy hyps concl (zboxes, prf) =
   let val (zbox, zbox_prf) = box_proof ZBox thy hyps concl prf