--- a/src/Pure/global_theory.ML Mon Dec 18 11:19:15 2023 +0100
+++ b/src/Pure/global_theory.ML Mon Dec 18 12:02:58 2023 +0100
@@ -243,7 +243,7 @@
name_multi name_pos #> map (uncurry (name_thm name_flags));
-(* apply theorems and attributes *)
+(* store theorems and proofs *)
fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy);
@@ -290,10 +290,17 @@
|> Lazy.map_finished (name_thms official1 name_pos #> map (Thm.kind_rule kind));
in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end;
+
+(* apply theorems and attributes *)
+
+local
+
val app_facts =
apfst flat oo fold_map (fn (thms, atts) => fn thy =>
fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy);
+in
+
fun apply_facts name_flags1 name_flags2 (b, facts) thy =
if Binding.is_empty b then app_facts facts thy |-> register_proofs
else
@@ -305,6 +312,8 @@
val thy'' = thy' |> add_facts (b, Lazy.value thms');
in (map (Thm.transfer thy'') thms', thy'') end;
+end;
+
(* store_thm *)