# HG changeset patch
# User wenzelm
# Date 1703422705 -3600
# Node ID 43d8385db923774773d19d5b0d3eb53ddbebec5d
# Parent  af7881b2299da7e5d16d93c9f5d397efa653a19e
more thorough thm definition via Global_Theory.register_proofs: store (and purge) zproofs;

diff -r af7881b2299d -r 43d8385db923 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Dec 24 13:20:40 2023 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sun Dec 24 13:58:25 2023 +0100
@@ -318,7 +318,9 @@
       |> Drule.zero_var_indexes_list;
 
     (*thm definition*)
-    val global_thm = Global_Theory.name_thm Global_Theory.official1 name schematic_thm;
+    val (global_thm, lthy') =
+      (Local_Theory.background_theory_result o yield_singleton (Global_Theory.register_proofs name))
+        (Global_Theory.name_thm Global_Theory.official1 name schematic_thm) lthy;
 
     (*import fixes*)
     val (tvars, vars) =
@@ -328,14 +330,14 @@
     val instT =
       TVars.build (fold2 (fn a => fn b =>
         (case a of TVar v => TVars.add (v, b) | _ => I)) tvars tfrees);
-    val cinstT = TVars.map (K (Thm.ctyp_of lthy)) instT;
+    val cinstT = TVars.map (K (Thm.ctyp_of lthy')) instT;
     val cinst =
       Vars.build
         (fold2 (fn v => fn t =>
           (case v of
             Var (xi, T) =>
               Vars.add ((xi, Term_Subst.instantiateT instT T),
-                Thm.cterm_of lthy (Term.map_types (Term_Subst.instantiateT instT) t))
+                Thm.cterm_of lthy' (Term.map_types (Term_Subst.instantiateT instT) t))
           | _ => I)) vars frees);
     val fixed_thm = Thm.instantiate (cinstT, cinst) global_thm;
 
@@ -347,7 +349,7 @@
       |> Goal.norm_result lthy
       |> Global_Theory.name_thm Global_Theory.unofficial2 name;
 
-  in ((local_thm, global_thm), lthy) end;
+  in ((local_thm, global_thm), lthy') end;
 
 fun name_thms name = split_list #>> burrow (Global_Theory.name_multi name) #> op ~~;
 
@@ -367,7 +369,7 @@
     val global_facts = Attrib.map_thms #2 facts';
   in
     lthy'
-    |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
+    |> target_notes kind global_facts (Attrib.partial_evaluation lthy' local_facts)
     |> Attrib.local_notes kind local_facts
   end;