# HG changeset patch
# User wenzelm
# Date 1572628772 -3600
# Node ID 2866fee241eecc21e9a9f70f1e9856937f469e44
# Parent  5e98925f86ede3a9bc68bf0d74a4b9455623c5b0
proper export of unnamed proof boxes for unnamed toplevel declarations, e.g. rulify/defn rules in theory IFOL and HOL;

diff -r 5e98925f86ed -r 2866fee241ee src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Fri Nov 01 18:08:46 2019 +0100
+++ b/src/Pure/global_theory.ML	Fri Nov 01 18:19:32 2019 +0100
@@ -288,10 +288,17 @@
     fold_map (Thm.theory_attributes atts) (map (Thm.transfer thy) thms) thy);
 
 fun apply_facts name_flags1 name_flags2 (b, facts) thy =
-  if Binding.is_empty b then app_facts facts thy |-> register_proofs
+  if Binding.is_empty b then
+    let
+      val (thms, thy') = app_facts facts thy;
+      val _ =
+        if Proofterm.export_proof_boxes_required thy' then
+          Proofterm.export_proof_boxes (map Thm.proof_of thms)
+        else ();
+    in register_proofs thms thy' end
   else
     let
-      val name_pos= bind_name thy b;
+      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;