# HG changeset patch
# User traytel
# Date 1395749673 -3600
# Node ID 159c07ceb18c3bfe0212ade190b0b83ab2c8626a
# Parent  61b1e3d88e91697eae360de54d8c524b95dd7501
prove theorems with fixed variables (export afterwards)

diff -r 61b1e3d88e91 -r 159c07ceb18c src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 24 14:51:10 2014 -0700
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Mar 25 13:14:33 2014 +0100
@@ -239,10 +239,10 @@
         val rhs =
           Term.list_comb (mapAsCs, take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
+        Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
           (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
@@ -257,10 +257,10 @@
         val prems = map4 mk_prem (drop m sets) self_fs zs zs';
         val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
           (K (mk_map_cong0L_tac m map_cong0 map_id))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
@@ -273,13 +273,12 @@
         val maps = map (fn mapx => Term.list_comb (mapx, all_gs)) mapsBsCs';
         val concls =
           map3 (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y)) yFs yFs_copy maps;
-        val goals =
-          map4 (fn prem => fn concl => fn x => fn y =>
-            fold_rev Logic.all (x :: y :: all_gs) (Logic.mk_implies (prem, concl)))
-          prems concls yFs yFs_copy;
+        val goals = map2 (fn prem => fn concl => Logic.mk_implies (prem, concl)) prems concls;
       in
-        map (fn goal => Goal.prove_sorry lthy [] [] goal
-          (K ((hyp_subst_tac lthy THEN' rtac refl) 1)) |> Thm.close_derivation) goals
+        map (fn goal =>
+          Goal.prove_sorry lthy [] [] goal (K ((hyp_subst_tac lthy THEN' rtac refl) 1))
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy)) goals
       end;
 
     val timer = time (timer "Derived simple theorems");
@@ -332,26 +331,27 @@
         val prems = map2 mk_prem zs Bs;
         val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets))
           ss zs setssAs;
-        val goalss = map3 (fn x => fn prem => fn concls => map (fn concl =>
-          fold_rev Logic.all (x :: Bs @ ss)
-            (Logic.list_implies (coalg_prem :: [prem], concl))) concls) zs prems conclss;
+        val goalss = map2 (fn prem => fn concls => map (fn concl =>
+          Logic.list_implies (coalg_prem :: [prem], concl)) concls) prems conclss;
       in
-        map (fn goals => map (fn goal => Goal.prove_sorry lthy [] [] goal
-          (K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss
+        map (fn goals => map (fn goal =>
+          Goal.prove_sorry lthy [] [] goal (K (mk_coalg_set_tac coalg_def))
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy)) goals) goalss
       end;
 
     fun mk_tcoalg BTs = mk_coalg (map HOLogic.mk_UNIV BTs);
 
     val tcoalg_thm =
       let
-        val goal = fold_rev Logic.all ss
-          (HOLogic.mk_Trueprop (mk_tcoalg activeAs ss))
+        val goal = HOLogic.mk_Trueprop (mk_tcoalg activeAs ss)
       in
         Goal.prove_sorry lthy [] [] goal
           (K (rtac (coalg_def RS iffD2) 1 THEN CONJ_WRAP
             (K (EVERY' [rtac ballI, rtac CollectI,
               CONJ_WRAP' (K (EVERY' [rtac @{thm subset_UNIV}])) allAs] 1)) ss))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val timer = time (timer "Coalgebra definition & thms");
@@ -401,17 +401,17 @@
     val (mor_image_thms, morE_thms) =
       let
         val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
-        fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
-          (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)));
+        fun mk_image_goal f B1 B2 =
+          Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2));
         val image_goals = map3 mk_image_goal fs Bs B's;
         fun mk_elim_goal B mapAsBs f s s' x =
-          fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
-            (Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))],
-              mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x))));
+          Logic.list_implies ([prem, HOLogic.mk_Trueprop (HOLogic.mk_mem (x, B))],
+            mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)));
         val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs;
         fun prove goal =
           Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
       in
         (map prove image_goals, map prove elim_goals)
       end;
@@ -423,10 +423,10 @@
         val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
           (K (mk_mor_incl_tac mor_def map_ids))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);
@@ -439,11 +439,10 @@
         val concl =
           HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
-            (Logic.list_implies (prems, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
           (K (mk_mor_comp_tac mor_def mor_image'_thms morE_thms map_comp_id_thms))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_cong_thm =
@@ -452,11 +451,10 @@
          (map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs])
         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
-            (Logic.list_implies (prems, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
           (K ((hyp_subst_tac lthy THEN' atac) 1))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_UNIV_thm =
@@ -467,9 +465,10 @@
         val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
         val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
       in
-        Goal.prove_sorry lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
+        Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
           (K (mk_mor_UNIV_tac morE_thms mor_def))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_str_thm =
@@ -478,10 +477,10 @@
           (mk_map_of_bnf Ds allAs (passiveAs @ FTsAs) bnf, passive_ids @ ss)) Dss bnfs;
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all ss (HOLogic.mk_Trueprop
-            (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss)))
+          (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss))
           (K (mk_mor_str_tac ks mor_UNIV_thm))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_case_sum_thm =
@@ -491,10 +490,10 @@
           s's sum_ss map_Inls;
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (s's @ sum_ss) (HOLogic.mk_Trueprop
-            (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls)))
+          (HOLogic.mk_Trueprop (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls))
           (K (mk_mor_case_sum_tac ks mor_UNIV_thm))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val timer = time (timer "Morphism definition & thms");
@@ -550,11 +549,10 @@
          (mk_bis Bs ss B's s's Rs :: map2 (curry HOLogic.mk_eq) Rs_copy Rs)
         val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy);
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
-            (Logic.list_implies (prems, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' atac) 1)
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val bis_rel_thm =
@@ -568,21 +566,19 @@
           (bis_le, Library.foldr1 HOLogic.mk_conj
             (map6 mk_conjunct Rs ss s's zs z's relsAsBs))
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
-            (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs)))
+        Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs))
           (K (mk_bis_rel_tac m bis_def in_rels map_comps map_cong0s set_mapss))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val bis_converse_thm =
       Goal.prove_sorry lthy [] []
-        (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
-          (Logic.mk_implies
-            (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
-            HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs)))))
+        (Logic.mk_implies (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
+          HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs))))
         (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converseps))
-      |> Thm.close_derivation;
+      |> Thm.close_derivation
+      |> singleton (Proof_Context.export names_lthy lthy);
 
     val bis_O_thm =
       let
@@ -592,11 +588,10 @@
         val concl =
           HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
-            (Logic.list_implies (prems, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
           (K (mk_bis_O_tac lthy m bis_rel_thm rel_congs rel_OOs))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val bis_Gr_thm =
@@ -604,12 +599,11 @@
         val concl =
           HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map2 mk_Gr Bs fs));
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
-            (Logic.list_implies ([coalg_prem, mor_prem], concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies ([coalg_prem, mor_prem], concl))
           (fn {context = ctxt, prems = _} => mk_bis_Gr_tac ctxt bis_rel_thm rel_Grps mor_image_thms
             morE_thms coalg_in_thms)
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val bis_image2_thm = bis_cong_thm OF
@@ -627,11 +621,10 @@
         val concl =
           HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map (mk_UNION Idx) Ris));
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Idx :: Bs @ ss @ B's @ s's @ Ris)
-            (Logic.mk_implies (prem, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, concl))
           (fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     (* self-bisimulation *)
@@ -677,11 +670,10 @@
       end;
 
     val sbis_lsbis_thm =
-      Goal.prove_sorry lthy [] []
-        (fold_rev Logic.all (Bs @ ss)
-          (HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks))))
+      Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_sbis Bs ss (map (mk_lsbis Bs ss) ks)))
         (K (mk_sbis_lsbis_tac lthy lsbis_defs bis_Union_thm bis_cong_thm))
-      |> Thm.close_derivation;
+      |> Thm.close_derivation
+      |> singleton (Proof_Context.export names_lthy lthy);
 
     val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
       (bis_def RS iffD1 RS conjunct1 RS mk_conjunctN n i)) ks;
@@ -691,24 +683,25 @@
     val incl_lsbis_thms =
       let
         fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis Bs ss i));
-        val goals = map2 (fn i => fn R => fold_rev Logic.all (Bs @ ss @ sRs)
-          (Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs;
+        val goals = map2 (fn i => fn R => Logic.mk_implies (sbis_prem, mk_concl i R)) ks sRs;
       in
-        map3 (fn goal => fn i => fn def => Goal.prove_sorry lthy [] [] goal
-          (K (mk_incl_lsbis_tac n i def)) |> Thm.close_derivation) goals ks lsbis_defs
+        map3 (fn goal => fn i => fn def =>
+          Goal.prove_sorry lthy [] [] goal (K (mk_incl_lsbis_tac n i def))
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy)) goals ks lsbis_defs
       end;
 
     val equiv_lsbis_thms =
       let
         fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis Bs ss i));
-        val goals = map2 (fn i => fn B => fold_rev Logic.all (Bs @ ss)
-          (Logic.mk_implies (coalg_prem, mk_concl i B))) ks Bs;
+        val goals = map2 (fn i => fn B => Logic.mk_implies (coalg_prem, mk_concl i B)) ks Bs;
       in
         map3 (fn goal => fn l_incl => fn incl_l =>
           Goal.prove_sorry lthy [] [] goal
             (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l
               bis_Id_on_thm bis_converse_thm bis_O_thm))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy))
         goals lsbis_incl_thms incl_lsbis_thms
       end;
 
@@ -1089,22 +1082,24 @@
 
         val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
 
-        val length_Lev = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+        val length_Lev =
+          Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
             (K (mk_length_Lev_tac lthy cts Lev_0s Lev_Sucs))
-          |> Thm.close_derivation);
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
 
         val length_Lev' = mk_specN (n + 1) length_Lev;
         val length_Levs = map (fn i => length_Lev' RS mk_conjunctN n i RS mp) ks;
 
-        fun mk_goal i z = fold_rev Logic.all (z :: kl :: nat :: ss) (Logic.mk_implies
+        fun mk_goal i z = Logic.mk_implies
             (HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z)),
-            HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z))));
+            HOLogic.mk_Trueprop (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z)));
         val goals = map2 mk_goal ks zs;
 
         val length_Levs' = map2 (fn goal => fn length_Lev =>
           Goal.prove_sorry lthy [] [] goal (K (mk_length_Lev'_tac length_Lev))
-          |> Thm.close_derivation) goals length_Levs;
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy)) goals length_Levs;
       in
         (length_Levs, length_Levs')
       end;
@@ -1123,10 +1118,11 @@
         val cTs = [SOME (certifyT lthy sum_sbdT)];
         val cts = map (SOME o certify lthy) [Term.absfree kl' goal, kl];
 
-        val rv_last = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss)))
-          |> Thm.close_derivation;
+        val rv_last =
+          Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+            (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss))
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
 
         val rv_last' = mk_specN (n + 1) rv_last;
       in
@@ -1158,10 +1154,11 @@
 
         val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
 
-        val set_Lev = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_set_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
-          |> Thm.close_derivation;
+        val set_Lev =
+          Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+            (K (mk_set_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss))
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
 
         val set_Lev' = mk_specN (3 * n + 1) set_Lev;
       in
@@ -1196,11 +1193,12 @@
 
         val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat];
 
-        val set_image_Lev = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+        val set_image_Lev =
+          Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
             (K (mk_set_image_Lev_tac lthy cts Lev_0s Lev_Sucs rv_Nils rv_Conss
-              from_to_sbd_thmss to_sbd_inj_thmss)))
-          |> Thm.close_derivation;
+              from_to_sbd_thmss to_sbd_inj_thmss))
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
 
         val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev;
       in
@@ -1212,14 +1210,14 @@
 
     val mor_beh_thm =
       Goal.prove_sorry lthy [] []
-        (fold_rev Logic.all ss (HOLogic.mk_Trueprop
-          (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks))))
+        (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks)))
         (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm
           beh_defs carT_defs strT_defs isNode_defs
           to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss
           length_Lev_thms length_Lev'_thms rv_last_thmss set_Lev_thmsss
           set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation
+      |> singleton (Proof_Context.export names_lthy lthy);
 
     val timer = time (timer "Behavioral morphism");
 
@@ -1397,11 +1395,11 @@
         val morEs' = map (fn thm => (thm OF [mor_final_thm, UNIV_I]) RS sym) morE_thms;
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all ss
-            (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks))))
+          (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks)))
           (K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs'
             map_comp_id_thms map_cong0s))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
     val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
 
@@ -1410,13 +1408,13 @@
         val prem = HOLogic.mk_Trueprop (mk_sbis UNIVs dtors TRs);
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts));
-        val goal = fold_rev Logic.all TRs (Logic.mk_implies (prem, concl));
       in
-        `split_conj_thm (Goal.prove_sorry lthy [] [] goal
+        `split_conj_thm (Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, concl))
           (K (mk_raw_coind_tac bis_def bis_cong_thm bis_O_thm bis_converse_thm bis_Gr_thm
             tcoalg_thm coalgT_thm mor_T_final_thm sbis_lsbis_thm
             lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy))
       end;
 
     val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
@@ -1429,10 +1427,10 @@
         val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
         val mor_thm = mor_comp_thm OF [mor_final_thm, mor_Abs_thm];
 
-        val unique_mor = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
+        val unique_mor = Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
           (K (mk_unfold_unique_mor_tac raw_coind_thms bis_thm mor_thm unfold_defs))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
       in
         `split_conj_thm unique_mor
       end;
@@ -1558,7 +1556,7 @@
             val lhs = dtor $ (mk_corec corec_ss i $ z);
             val rhs = Term.list_comb (corec_map, passive_ids @ case_sums) $ (corec_s $ z);
           in
-            fold_rev Logic.all (z :: corec_ss) (mk_Trueprop_eq (lhs, rhs))
+            mk_Trueprop_eq (lhs, rhs)
           end;
         val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
       in
@@ -1566,7 +1564,8 @@
           Goal.prove_sorry lthy [] [] goal
             (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0
               corec_Inl_sum_thms)
-          |> Thm.close_derivation)
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy))
         goals dtor_unfold_thms map_cong0s
       end;
 
@@ -1578,11 +1577,11 @@
         val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (map2 mk_fun_eq unfold_fs ks));
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (corec_ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
+        Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
           (fn {context = ctxt, prems = _} => mk_corec_unique_mor_tac ctxt corec_defs
             corec_Inl_sum_thms unfold_unique_mor_thm)
           |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val map_id0s_o_id =
@@ -1601,9 +1600,6 @@
 
     val (coinduct_params, dtor_coinduct_thm) =
       let
-        val zs = Jzs1 @ Jzs2;
-        val frees = phis @ zs;
-
         val rels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
 
         fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
@@ -1620,13 +1616,13 @@
           end;
 
         val rel_prems = map5 mk_rel_prem phis dtors rels Jzs Jzs_copy;
-        val dtor_coinduct_goal =
-          fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
+        val dtor_coinduct_goal = Logic.list_implies (rel_prems, concl);
 
         val dtor_coinduct =
           Goal.prove_sorry lthy [] [] dtor_coinduct_goal
             (K (mk_dtor_coinduct_tac m raw_coind_thm bis_rel_thm rel_congs))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
       in
         (rev (Term.add_tfrees dtor_coinduct_goal []), dtor_coinduct)
       end;
@@ -1788,16 +1784,16 @@
 
         val (dtor_Jmap_thms, Jmap_thms) =
           let
-            fun mk_goal fs_Jmap map dtor dtor' = fold_rev Logic.all fs
-              (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap),
-                HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor)));
+            fun mk_goal fs_Jmap map dtor dtor' = mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap),
+              HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor));
             val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's;
             val maps =
               map5 (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong =>
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
                      mk_map_tac m n map_arg_cong unfold map_comp map_cong0)
-                |> Thm.close_derivation)
+                |> Thm.close_derivation
+                |> singleton (Proof_Context.export names_lthy lthy))
               goals dtor_unfold_thms map_comps map_cong0s map_arg_cong_thms;
           in
             map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
@@ -1813,24 +1809,24 @@
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                 (map2 (curry HOLogic.mk_eq) us fs_Jmaps));
           in
-            Goal.prove_sorry lthy [] []
-              (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
-                (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
-                  mk_dtor_map_unique_tac ctxt dtor_unfold_unique_thm sym_map_comps)
-              |> Thm.close_derivation
+            Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
+              (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
+                mk_dtor_map_unique_tac ctxt dtor_unfold_unique_thm sym_map_comps)
+            |> Thm.close_derivation
+            |> singleton (Proof_Context.export names_lthy lthy)
           end;
 
         val Jmap_comp0_thms =
           let
-            val goal = fold_rev Logic.all (fs @ gs)
-              (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-                (map3 (fn fmap => fn gmap => fn fgmap =>
-                   HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
-                fs_Jmaps gs_Jmaps fgs_Jmaps)))
+            val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+              (map3 (fn fmap => fn gmap => fn fgmap =>
+                 HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
+              fs_Jmaps gs_Jmaps fgs_Jmaps))
           in
             split_conj_thm (Goal.prove_sorry lthy [] [] goal
               (K (mk_map_comp0_tac Jmap_thms map_comp0s dtor_Jmap_unique_thm))
-              |> Thm.close_derivation)
+              |> Thm.close_derivation
+              |> singleton (Proof_Context.export names_lthy lthy))
           end;
 
         val timer = time (timer "map functions for the new codatatypes");
@@ -1865,11 +1861,11 @@
                   map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
               in
                 map4 (fn goal => fn cts => fn col_0s => fn col_Sucs =>
-                  singleton (Proof_Context.export names_lthy lthy)
-                    (Goal.prove_sorry lthy [] [] goal
-                      (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
-                        col_Sucs))
-                  |> Thm.close_derivation)
+                  Goal.prove_sorry lthy [] [] goal
+                    (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
+                      col_Sucs)
+                  |> Thm.close_derivation
+                  |> singleton (Proof_Context.export names_lthy lthy))
                 goals ctss col_0ss' col_Sucss'
               end;
     
@@ -1877,27 +1873,26 @@
             fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct sets Ks Jzs);
             val concls = map2 mk_concl Jsetss_by_range Kss;
     
-            val goals = map3 (fn Ks => fn prems => fn concl =>
-              fold_rev Logic.all (Ks @ Jzs)
-                (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls;
+            val goals = map2 (fn prems => fn concl =>
+              Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls;
           in
             map2 (fn goal => fn col_minimal =>
               Goal.prove_sorry lthy [] [] goal
                 (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
                   mk_Jset_minimal_tac ctxt n col_minimal)
-              |> Thm.close_derivation)
+              |> Thm.close_derivation
+              |> singleton (Proof_Context.export names_lthy lthy))
             goals col_minimal_thms
           end;
 
         val (dtor_Jset_incl_thmss, dtor_set_Jset_incl_thmsss) =
           let
-            fun mk_set_incl_Jset dtor x set Jset = fold_rev Logic.all (x :: ss)
-              (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (Jset $ x)));
+            fun mk_set_incl_Jset dtor x set Jset =
+              HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (Jset $ x));
     
             fun mk_set_Jset_incl_Jset dtor x y set Jset1 Jset2 =
-              fold_rev Logic.all [x, y]
-                (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))),
-                HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y))));
+              Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))),
+                HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y)));
     
             val set_incl_Jset_goalss =
               map4 (fn dtor => fn x => fn sets => fn Jsets =>
@@ -1917,7 +1912,8 @@
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
                     mk_set_incl_Jset_tac rec_Suc)
-                |> Thm.close_derivation)
+                |> Thm.close_derivation
+                |> singleton (Proof_Context.export names_lthy lthy))
               goals rec_Sucs)
             set_incl_Jset_goalss col_Sucss,
             map2 (fn goalss => fn rec_Sucs =>
@@ -1926,7 +1922,8 @@
                   Goal.prove_sorry lthy [] [] goal
                     (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
                       mk_set_Jset_incl_Jset_tac n rec_Suc k)
-                  |> Thm.close_derivation)
+                  |> Thm.close_derivation
+                  |> singleton (Proof_Context.export names_lthy lthy))
                 goals rec_Sucs)
               ks goalss)
             set_Jset_incl_Jset_goalsss col_Sucss)
@@ -1977,24 +1974,23 @@
                 FTs_setss dtors Jzs sets)
               ls Jsetss_by_range;
 
-            val le_goals = map
-              (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
+            val le_goals = map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
               (mk_goals (uncurry mk_leq));
             val set_le_thmss = map split_conj_thm
               (map4 (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss =>
                 Goal.prove_sorry lthy [] [] goal
                   (K (mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation
+                |> singleton (Proof_Context.export names_lthy lthy))
               le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss');
 
-            val ge_goalss = map (map2 (fn z => fn goal =>
-                Logic.all z (HOLogic.mk_Trueprop goal)) Jzs)
-              (mk_goals (uncurry mk_leq o swap));
+            val ge_goalss = map (map HOLogic.mk_Trueprop) (mk_goals (uncurry mk_leq o swap));
             val set_ge_thmss = 
               map3 (map3 (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
                 Goal.prove_sorry lthy [] [] goal
                   (K (mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets))
-                |> Thm.close_derivation))
+                |> Thm.close_derivation
+                |> singleton (Proof_Context.export names_lthy lthy)))
               ge_goalss set_incl_Jset_thmss' set_Jset_incl_Jset_thmsss'
           in
             map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss
@@ -2023,11 +2019,11 @@
 
             val thms =
               map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
-                singleton (Proof_Context.export names_lthy lthy)
-                  (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-                    (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs
-                      dtor_Jmap_thms set_mapss))
-                |> Thm.close_derivation)
+                Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+                  (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs
+                    dtor_Jmap_thms set_mapss)
+                |> Thm.close_derivation
+                |> singleton (Proof_Context.export names_lthy lthy))
               goals ctss col_0ss' col_Sucss';
           in
             map (split_conj_thm o mk_specN n) thms
@@ -2047,11 +2043,11 @@
 
             val thms =
               map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
-                singleton (Proof_Context.export names_lthy lthy)
-                  (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-                    (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN
-                      mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss))
-                |> Thm.close_derivation)
+                Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+                  (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN
+                    mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss)
+                |> Thm.close_derivation
+                |> singleton (Proof_Context.export names_lthy lthy))
               ls goals ctss col_0ss' col_Sucss';
           in
             map (split_conj_thm o mk_specN n) thms
@@ -2092,11 +2088,12 @@
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                 (map4 mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps));
 
-            val thm = singleton (Proof_Context.export names_lthy lthy)
-              (Goal.prove_sorry lthy [] [] goal
+            val thm =
+              Goal.prove_sorry lthy [] [] goal
                 (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s
-                  set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels)))
+                  set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels))
               |> Thm.close_derivation
+              |>  singleton (Proof_Context.export names_lthy lthy);
           in
             split_conj_thm thm
           end;
@@ -2114,8 +2111,8 @@
 
         val dtor_Jrel_thms =
           let
-            fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
-              (mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz')));
+            fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi =
+              mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz'));
             val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
           in
             map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
@@ -2124,7 +2121,8 @@
               Goal.prove_sorry lthy [] [] goal
                 (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
                   dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss))
-              |> Thm.close_derivation)
+              |> Thm.close_derivation
+              |> singleton (Proof_Context.export names_lthy lthy))
             ks goals in_rels map_comps map_cong0s dtor_Jmap_thms dtor_Jset_thmss'
               dtor_inject_thms dtor_ctor_thms set_mapss dtor_Jset_incl_thmss
               dtor_set_Jset_incl_thmsss
@@ -2261,10 +2259,10 @@
 
             val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
           in
-            singleton (Proof_Context.export names_lthy lthy)
-              (Goal.prove_sorry lthy [] [] goal
-                (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms rel_OOs)))
-              |> Thm.close_derivation
+            Goal.prove_sorry lthy [] [] goal
+              (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms rel_OOs))
+            |> Thm.close_derivation
+            |> singleton (Proof_Context.export names_lthy lthy)
           end;
 
         val timer = time (timer "helpers for BNF properties");
@@ -2374,8 +2372,8 @@
                         else @{term False})
                     else @{term True}));
               in
-                fold_rev Logic.all (map (nth ys) I @ Jzs) (HOLogic.mk_Trueprop
-                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits)))
+                HOLogic.mk_Trueprop
+                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits))
               end;
             val goals = map5 mk_goal Jsetss_by_range ys ys_copy ys'_copy ls;
           in
@@ -2383,7 +2381,8 @@
               Goal.prove_sorry lthy [] [] goal
                 (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms
                   (flat set_mapss) wit_thms)
-              |> Thm.close_derivation)
+              |> Thm.close_derivation
+              |> singleton (Proof_Context.export names_lthy lthy))
             goals dtor_Jset_induct_thms
             |> map split_conj_thm
             |> transpose
diff -r 61b1e3d88e91 -r 159c07ceb18c src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 24 14:51:10 2014 -0700
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 25 13:14:33 2014 +0100
@@ -207,10 +207,10 @@
         val rhs = Term.list_comb (mapAsCs,
           take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
+        Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
           (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
@@ -224,10 +224,10 @@
         val prems = map4 mk_prem (drop m sets) self_fs zs zs';
         val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
           (K (mk_map_cong0L_tac m map_cong0 map_id))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
@@ -278,12 +278,13 @@
         fun mk_concl s x B = HOLogic.mk_Trueprop (HOLogic.mk_mem (s $ x, B));
         val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs;
         val concls = map3 mk_concl ss xFs Bs;
-        val goals = map3 (fn x => fn prems => fn concl =>
-          fold_rev Logic.all (x :: Bs @ ss)
-            (Logic.list_implies (alg_prem :: prems, concl))) xFs premss concls;
+        val goals = map2 (fn prems => fn concl =>
+          Logic.list_implies (alg_prem :: prems, concl)) premss concls;
       in
         map (fn goal =>
-          Goal.prove_sorry lthy [] [] goal (K (mk_alg_set_tac alg_def)) |> Thm.close_derivation)
+          Goal.prove_sorry lthy [] [] goal (K (mk_alg_set_tac alg_def))
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy))
         goals
       end;
 
@@ -295,13 +296,13 @@
           HOLogic.mk_Trueprop (mk_alg Bs ss);
         val concls = map (HOLogic.mk_Trueprop o mk_not_empty) Bs;
         val goals =
-          map (fn concl =>
-            fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (alg_prem, concl))) concls;
+          map (fn concl => Logic.mk_implies (alg_prem, concl)) concls;
       in
         map2 (fn goal => fn alg_set =>
-          Goal.prove_sorry lthy [] []
-            goal (K (mk_alg_not_empty_tac lthy alg_set alg_set_thms wit_thms))
-          |> Thm.close_derivation)
+          Goal.prove_sorry lthy [] [] goal
+            (K (mk_alg_not_empty_tac lthy alg_set alg_set_thms wit_thms))
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy))
         goals alg_set_thms
       end;
 
@@ -355,12 +356,12 @@
         fun mk_elim_prem sets x T = HOLogic.mk_Trueprop
           (HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T));
         fun mk_elim_goal sets mapAsBs f s s' x T =
-          fold_rev Logic.all (x :: Bs @ ss @ B's @ s's @ fs)
-            (Logic.list_implies ([prem, mk_elim_prem sets x T],
-              mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x]))));
+          Logic.list_implies ([prem, mk_elim_prem sets x T],
+            mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x])));
         val elim_goals = map7 mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
-        fun prove goal =
-          Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
+        fun prove goal = Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def))
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
       in
         map prove elim_goals
       end;
@@ -370,10 +371,10 @@
         val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
           (K (mk_mor_incl_tac mor_def map_ids))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_comp_thm =
@@ -384,11 +385,10 @@
         val concl =
           HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
-             (Logic.list_implies (prems, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
           (K (mk_mor_comp_tac mor_def set_mapss map_comp_id_thms))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_cong_thm =
@@ -397,11 +397,10 @@
          (map2 (curry HOLogic.mk_eq) fs_copy fs @ [mk_mor Bs ss B's s's fs])
         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
-             (Logic.list_implies (prems, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
           (K ((hyp_subst_tac lthy THEN' atac) 1))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_str_thm =
@@ -410,10 +409,11 @@
           (mk_map_of_bnf Ds (passiveAs @ FTsAs) allAs bnf, passive_ids @ ss)) Dss bnfs;
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all ss (HOLogic.mk_Trueprop
-            (mk_mor (map HOLogic.mk_UNIV FTsAs) maps active_UNIVs ss ss)))
+          (HOLogic.mk_Trueprop
+            (mk_mor (map HOLogic.mk_UNIV FTsAs) maps active_UNIVs ss ss))
           (K (mk_mor_str_tac ks mor_def))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_convol_thm =
@@ -423,10 +423,11 @@
           s's prod_ss map_fsts;
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (s's @ prod_ss) (HOLogic.mk_Trueprop
-            (mk_mor prod_UNIVs maps (map HOLogic.mk_UNIV activeBs) s's fsts)))
+          (HOLogic.mk_Trueprop
+            (mk_mor prod_UNIVs maps (map HOLogic.mk_UNIV activeBs) s's fsts))
           (K (mk_mor_convol_tac ks mor_def))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_UNIV_thm =
@@ -437,9 +438,10 @@
         val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
         val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
       in
-        Goal.prove_sorry lthy [] [] (fold_rev Logic.all (ss @ s's @ fs) (mk_Trueprop_eq (lhs, rhs)))
+        Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
           (K (mk_mor_UNIV_tac m morE_thms mor_def))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val timer = time (timer "Morphism definition & thms");
@@ -553,10 +555,10 @@
         val concl = HOLogic.mk_Trueprop (mk_Bex field_suc_bd
           (Term.absfree jdx' (Library.foldr1 HOLogic.mk_conj (map mk_conjunct idxs))));
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all idxs (Logic.list_implies ([prem], concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies ([prem], concl))
           (K (mk_bd_limit_tac n suc_bd_Cinfinite))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val timer = time (timer "Bounds");
@@ -592,23 +594,23 @@
         val concl = HOLogic.mk_Trueprop
           (HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
             (map4 (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
-        val goal = fold_rev Logic.all (idx :: ss)
-          (Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl));
+        val goal = Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl);
 
         val min_algs_thm = Goal.prove_sorry lthy [] [] goal
           (K (mk_min_algs_tac suc_bd_worel in_cong'_thms))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
 
         val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
 
         fun mk_mono_goal min_alg =
-          fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_relChain suc_bd
-            (Term.absfree idx' min_alg)));
+          HOLogic.mk_Trueprop (mk_relChain suc_bd (Term.absfree idx' min_alg));
 
         val monos =
           map2 (fn goal => fn min_algs =>
             Goal.prove_sorry lthy [] [] goal (K (mk_min_algs_mono_tac lthy min_algs))
-            |> Thm.close_derivation)
+            |> Thm.close_derivation
+            |> singleton (Proof_Context.export names_lthy lthy))
           (map mk_mono_goal min_algss) min_algs_thms;
 
         fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
@@ -616,27 +618,29 @@
         val card_cT = certifyT lthy suc_bdT;
         val card_ct = certify lthy (Term.absfree idx' card_conjunction);
 
-        val card_of = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] []
+        val card_of =
+          Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, card_conjunction)))
             (K (mk_min_algs_card_of_tac card_cT card_ct
               m suc_bd_worel min_algs_thms in_sbds
               sbd_Card_order sbd_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
-              suc_bd_Asuc_bd Asuc_bd_Cinfinite)))
-          |> Thm.close_derivation;
+              suc_bd_Asuc_bd Asuc_bd_Cinfinite))
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
 
         val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
         val least_cT = certifyT lthy suc_bdT;
         val least_ct = certify lthy (Term.absfree idx' least_conjunction);
 
-        val least = singleton (Proof_Context.export names_lthy lthy)
+        val least =
           (Goal.prove_sorry lthy [] []
             (Logic.mk_implies (least_prem,
               HOLogic.mk_Trueprop (HOLogic.mk_imp (i_field, least_conjunction))))
             (K (mk_min_algs_least_tac least_cT least_ct
               suc_bd_worel min_algs_thms alg_set_thms)))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
       in
         (min_algs_thms, monos, card_of, least)
       end;
@@ -680,11 +684,12 @@
 
     val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) =
       let
-        val goal = fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_alg min_algs ss));
+        val goal = HOLogic.mk_Trueprop (mk_alg min_algs ss);
         val alg_min_alg = Goal.prove_sorry lthy [] [] goal
           (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sbd_Cinfinite
             set_sbdss min_algs_thms min_algs_mono_thms))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
 
         fun mk_card_of_thm min_alg def = Goal.prove_sorry lthy [] []
           (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd))
@@ -694,20 +699,20 @@
 
         val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         fun mk_least_thm min_alg B def = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss)
-            (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B))))
+          (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_leq min_alg B)))
           (K (mk_least_min_alg_tac def least_min_algs_thm))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
 
         val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
 
         val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val incl = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss)
-            (Logic.mk_implies (incl_prem,
-              HOLogic.mk_Trueprop (mk_mor min_algs ss Bs ss active_ids))))
+          (Logic.mk_implies (incl_prem,
+              HOLogic.mk_Trueprop (mk_mor min_algs ss Bs ss active_ids)))
           (K (EVERY' (rtac mor_incl_thm :: map etac leasts) 1))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
       in
         (alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl)
       end;
@@ -803,11 +808,11 @@
           (mk_mor car_inits str_inits active_UNIVs ss
             (map (fn f => HOLogic.mk_comp (f, mk_rapp iidx Asuc_bdT)) Asuc_fs));
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (iidx :: ss @ Asuc_fs) (Logic.list_implies (prems, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
           (K (mk_mor_select_tac mor_def mor_cong_thm mor_comp_thm mor_incl_min_alg_thm alg_def
             alg_select_thm alg_set_thms set_mapss str_init_defs))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val init_unique_mor_thms =
@@ -820,13 +825,12 @@
         val unique = HOLogic.mk_Trueprop
           (Library.foldr1 HOLogic.mk_conj (map3 mk_fun_eq init_fs init_fs_copy init_xs));
         val cts = map (certify lthy) ss;
-        val unique_mor = singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] []
-            (fold_rev Logic.all (init_xs @ Bs @ init_fs @ init_fs_copy)
-              (Logic.list_implies (prems @ mor_prems, unique)))
+        val unique_mor =
+          Goal.prove_sorry lthy [] [] (Logic.list_implies (prems @ mor_prems, unique))
             (K (mk_init_unique_mor_tac cts m alg_def alg_init_thm least_min_alg_thms
               in_mono'_thms alg_set_thms morE_thms map_cong0s))
-          |> Thm.close_derivation);
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
       in
         split_conj_thm unique_mor
       end;
@@ -856,10 +860,10 @@
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (map2 mk_Ball car_inits init_phis));
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all init_phis (Logic.mk_implies (prem, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, concl))
           (K (mk_init_induct_tac m alg_def alg_init_thm least_min_alg_thms alg_set_thms))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val timer = time (timer "Initiality definition & thms");
@@ -1005,10 +1009,10 @@
         val concl = HOLogic.mk_Trueprop (list_exists_free s's
           (HOLogic.mk_conj (mk_alg B's s's, mk_mor B's s's Bs ss inv_fs)));
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs) (Logic.list_implies (prems, concl)))
+        Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
           (K (mk_copy_tac m alg_def mor_def alg_set_thms set_mapss))
           |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val init_ex_mor_thm =
@@ -1016,12 +1020,12 @@
         val goal = HOLogic.mk_Trueprop
           (list_exists_free fs (mk_mor UNIVs ctors active_UNIVs ss fs));
       in
-        singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] [] goal
-            (fn {context = ctxt, prems = _} =>
-              mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm (alg_min_alg_thm RS copy_thm)
-                card_of_min_alg_thms mor_Rep_thm mor_comp_thm mor_select_thm mor_incl_thm)
-            |> Thm.close_derivation)
+        Goal.prove_sorry lthy [] [] goal
+          (fn {context = ctxt, prems = _} =>
+            mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm (alg_min_alg_thm RS copy_thm)
+              card_of_min_alg_thms mor_Rep_thm mor_comp_thm mor_select_thm mor_incl_thm)
+        |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_fold_thm =
@@ -1030,11 +1034,11 @@
         val cT = certifyT lthy foldT;
         val ct = certify lthy fold_fun
       in
-        singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] []
-            (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
-            (K (mk_mor_fold_tac cT ct fold_defs init_ex_mor_thm mor_cong)))
+        Goal.prove_sorry lthy [] []
+          (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
+          (K (mk_mor_fold_tac cT ct fold_defs init_ex_mor_thm mor_cong))
         |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
@@ -1046,11 +1050,11 @@
         val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss fs);
         fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_fold Ts ss i);
         val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
-        val unique_mor = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (ss @ fs) (Logic.mk_implies (prem, unique)))
+        val unique_mor = Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
           (K (mk_fold_unique_mor_tac type_defs init_unique_mor_thms Reps
             mor_comp_thm mor_Abs_thm mor_fold_thm))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy);
       in
         `split_conj_thm unique_mor
       end;
@@ -1175,14 +1179,15 @@
             val lhs = mk_rec rec_ss i $ (ctor $ x);
             val rhs = rec_s $ (Term.list_comb (rec_map, passive_ids @ convols) $ x);
           in
-            fold_rev Logic.all (x :: rec_ss) (mk_Trueprop_eq (lhs, rhs))
+            mk_Trueprop_eq (lhs, rhs)
           end;
         val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
       in
         map2 (fn goal => fn foldx =>
           Goal.prove_sorry lthy [] [] goal
             (fn {context = ctxt, prems = _} => mk_rec_tac ctxt rec_defs foldx fst_rec_pair_thms)
-          |> Thm.close_derivation)
+          |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy))
         goals ctor_fold_thms
       end;
 
@@ -1193,11 +1198,11 @@
         fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_rec rec_ss i);
         val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
       in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (rec_ss @ fs) (Logic.mk_implies (prem, unique)))
+        Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
           (fn {context = ctxt, prems = _} => mk_rec_unique_mor_tac ctxt rec_defs fst_rec_pair_thms
             fold_unique_mor_thm)
           |> Thm.close_derivation
+          |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val (ctor_rec_unique_thms, ctor_rec_unique_thm) =
@@ -1234,11 +1239,11 @@
 
         val goal = Logic.list_implies (prems, concl);
       in
-        (Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (phis @ Izs) goal)
+        (Goal.prove_sorry lthy [] [] goal
           (K (mk_ctor_induct_tac lthy m set_mapss init_induct_thm morE_thms mor_Abs_thm
             Rep_inverses Abs_inverses Reps))
-        |> Thm.close_derivation,
+        |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy),
         rev (Term.add_tfrees goal []))
       end;
 
@@ -1277,11 +1282,11 @@
         val cts = map3 (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
         val goal = Logic.list_implies (prems, concl);
       in
-        (singleton (Proof_Context.export names_lthy lthy)
-          (Goal.prove_sorry lthy [] [] goal
-            (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
-              weak_ctor_induct_thms))
-          |> Thm.close_derivation,
+        (Goal.prove_sorry lthy [] [] goal
+          (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
+            weak_ctor_induct_thms)
+        |> Thm.close_derivation
+        |> singleton (Proof_Context.export names_lthy lthy),
         rev (Term.add_tfrees goal []))
       end;
 
@@ -1415,16 +1420,17 @@
 
         val (ctor_Imap_thms, ctor_Imap_o_thms) =
           let
-            fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs
-              (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
-                HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_Imaps))));
+            fun mk_goal fs_map map ctor ctor' =
+              mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
+                HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_Imaps)));
             val goals = map4 mk_goal fs_Imaps map_FTFT's ctors ctor's;
             val maps =
               map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
                     mk_map_tac m n foldx map_comp_id map_cong0)
-                |> Thm.close_derivation)
+                |> Thm.close_derivation
+                 |> singleton (Proof_Context.export names_lthy lthy))
               goals ctor_fold_thms map_comp_id_thms map_cong0s;
           in
             `(map (fn thm => thm RS @{thm comp_eq_dest})) maps
@@ -1439,11 +1445,11 @@
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                 (map2 (curry HOLogic.mk_eq) us fs_Imaps));
-            val unique = Goal.prove_sorry lthy [] []
-              (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
+            val unique = Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
               (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
                 mk_ctor_map_unique_tac ctxt ctor_fold_unique_thm sym_map_comps)
-              |> Thm.close_derivation;
+              |> Thm.close_derivation
+              |> singleton (Proof_Context.export names_lthy lthy);
           in
             `split_conj_thm unique
           end;
@@ -1464,9 +1470,9 @@
               ctor_fold_thms) goalss;
 
             fun mk_simp_goal pas_set act_sets sets ctor z set =
-              Logic.all z (mk_Trueprop_eq (set $ (ctor $ z),
+              mk_Trueprop_eq (set $ (ctor $ z),
                 mk_union (pas_set $ z,
-                  Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets))));
+                  Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)));
             val simp_goalss =
               map2 (fn i => fn sets =>
                 map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
@@ -1476,7 +1482,8 @@
             val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
                 Goal.prove_sorry lthy [] [] goal
                   (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats)))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation
+                |> singleton (Proof_Context.export names_lthy lthy))
               set_mapss) ls simp_goalss setss;
           in
             ctor_setss
@@ -1520,10 +1527,10 @@
             fun mk_tac ctxt induct = mk_set_nat_tac ctxt m (rtac induct) set_mapss ctor_Imap_thms;
             val thms =
               map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
-                singleton (Proof_Context.export names_lthy lthy)
-                  (Goal.prove_sorry lthy [] [] goal
-                    (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i))
-                |> Thm.close_derivation)
+                Goal.prove_sorry lthy [] [] goal
+                  (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i)
+                |> Thm.close_derivation
+                |> singleton (Proof_Context.export names_lthy lthy))
               goals csetss ctor_Iset_thmss inducts ls;
           in
             map split_conj_thm thms
@@ -1548,11 +1555,11 @@
             fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sbd_Cinfinite set_sbdss;
             val thms =
               map4 (fn goal => fn ctor_sets => fn induct => fn i =>
-                singleton (Proof_Context.export names_lthy lthy)
-                  (Goal.prove_sorry lthy [] [] goal
+                Goal.prove_sorry lthy [] [] goal
                     (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
-                      mk_tac ctxt induct ctor_sets i))
-                |> Thm.close_derivation)
+                      mk_tac ctxt induct ctor_sets i)
+                |> Thm.close_derivation
+                |> singleton (Proof_Context.export names_lthy lthy))
               goals ctor_Iset_thmss inducts ls;
           in
             map split_conj_thm thms
@@ -1579,11 +1586,11 @@
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                 (map4 mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps));
 
-            val thm = singleton (Proof_Context.export names_lthy lthy)
-              (Goal.prove_sorry lthy [] [] goal
-              (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac induct) set_Iset_thmsss
-                map_cong0s ctor_Imap_thms))
-              |> Thm.close_derivation;
+            val thm = Goal.prove_sorry lthy [] [] goal
+                (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac induct) set_Iset_thmsss
+                  map_cong0s ctor_Imap_thms)
+              |> Thm.close_derivation
+              |> singleton (Proof_Context.export names_lthy lthy);
           in
             split_conj_thm thm
           end;
@@ -1606,8 +1613,8 @@
 
         val ctor_Irel_thms =
           let
-            fun mk_goal xF yF ctor ctor' Irelphi relphi = fold_rev Logic.all (xF :: yF :: Iphis)
-              (mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF));
+            fun mk_goal xF yF ctor ctor' Irelphi relphi =
+              mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF);
             val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
           in
             map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
@@ -1616,7 +1623,8 @@
               Goal.prove_sorry lthy [] [] goal
                (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
                  ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss))
-              |> Thm.close_derivation)
+              |> Thm.close_derivation
+              |> singleton (Proof_Context.export names_lthy lthy))
             ks goals in_rels map_comps map_cong0s ctor_Imap_thms ctor_Iset_thmss'
               ctor_inject_thms ctor_dtor_thms set_mapss ctor_Iset_incl_thmss
               ctor_set_Iset_incl_thmsss
@@ -1637,11 +1645,11 @@
 
             val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
           in
-            singleton (Proof_Context.export names_lthy lthy)
-              (Goal.prove_sorry lthy [] [] goal
-                (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
-                  ctor_Irel_thms rel_mono_strongs rel_OOs))
-              |> Thm.close_derivation
+            Goal.prove_sorry lthy [] [] goal
+              (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
+                ctor_Irel_thms rel_mono_strongs rel_OOs)
+            |> Thm.close_derivation
+            |> singleton (Proof_Context.export names_lthy lthy)
           end;
 
         val timer = time (timer "helpers for BNF properties");