# HG changeset patch
# User traytel
# Date 1346753419 -7200
# Node ID 0e5b859e1c91f9658c914c0cb6457f7b5bb4a883
# Parent  61e222517d06ae964936e9553560b14bb8ded767
no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;

diff -r 61e222517d06 -r 0e5b859e1c91 src/HOL/Codatatype/Tools/bnf_comp.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Tue Sep 04 00:16:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Tue Sep 04 12:10:19 2012 +0200
@@ -188,8 +188,10 @@
       if ! quick_and_dirty then
         replicate ilive no_thm
       else
-        map (fn goal => Skip_Proof.prove lthy [] [] goal
-        (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer))))
+        map (fn goal =>
+          Skip_Proof.prove lthy [] [] goal
+            (fn {context, ...} => (mk_comp_set_alt_tac context (collect_set_natural_of_bnf outer)))
+          |> Thm.close_derivation)
         (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) comp_sets comp_sets_alt);
 
     fun comp_map_cong_tac _ =
@@ -227,6 +229,7 @@
         in
           Skip_Proof.prove lthy [] [] goal
             (fn {context, ...} => mk_comp_in_alt_tac context comp_set_alt_thms)
+          |> Thm.close_derivation
         end;
 
     fun comp_in_bd_tac _ =
@@ -346,7 +349,7 @@
           val goal =
             fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (killN_in, killN_in_alt)));
         in
-          Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac)
+          Skip_Proof.prove lthy [] [] goal (K killN_in_alt_tac) |> Thm.close_derivation
         end;
 
     fun killN_in_bd_tac _ =
@@ -455,7 +458,7 @@
           val goal =
             fold_rev Logic.all Asets (HOLogic.mk_Trueprop (HOLogic.mk_eq (liftN_in, liftN_in_alt)))
         in
-          Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac)
+          Skip_Proof.prove lthy [] [] goal (K liftN_in_alt_tac) |> Thm.close_derivation
         end;
 
     fun liftN_in_bd_tac _ =
@@ -543,6 +546,7 @@
               (HOLogic.mk_Trueprop (HOLogic.mk_eq (permute_in, permute_in_alt)));
         in
           Skip_Proof.prove lthy [] [] goal (K (mk_permute_in_alt_tac src dest))
+          |> Thm.close_derivation
         end;
 
     fun permute_in_bd_tac _ =
@@ -731,13 +735,13 @@
     val pred_unfold = Local_Defs.unfold lthy'
       (map unfold_defs (filter_refl (pred_unfolds_of unfold))) pred_def;
 
-    fun note thmN thms =
-      snd o Local_Theory.note
-        ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
+    val notes =
+      [(rel_unfoldN, [rel_unfold]),
+      (pred_unfoldN, [pred_unfold])]
+      |> map (fn (thmN, thms) =>
+        ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
   in
-    (bnf', lthy'
-      |> note rel_unfoldN [rel_unfold]
-      |> note pred_unfoldN [pred_unfold])
+    (bnf', lthy' |> Local_Theory.notes notes |> snd)
   end;
 
 fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) =
diff -r 61e222517d06 -r 0e5b859e1c91 src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 04 00:16:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 04 12:10:19 2012 +0200
@@ -829,11 +829,7 @@
       let
         val (axioms, wit_thms) = apfst (mk_axioms live) (chop (length goals) thms);
 
-        val bd_Card_order =
-          Skip_Proof.prove lthy [] []
-            (HOLogic.mk_Trueprop (mk_Card_order (bnf_bd_As)))
-            (fn _ => mk_Card_order_tac (#bd_card_order axioms));
-
+        val bd_Card_order = #bd_card_order axioms RS @{thm conjunct2[OF card_order_on_Card_order]};
         val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order];
         val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
 
@@ -855,6 +851,7 @@
           in
             Skip_Proof.prove lthy [] [] goal
               (fn {context = ctxt, ...} => mk_collect_set_natural_tac ctxt (#set_natural axioms))
+            |> Thm.close_derivation
           end;
 
         val collect_set_natural = mk_lazy mk_collect_set_natural;
@@ -868,6 +865,7 @@
                   (mk_subset (mk_in As bnf_sets_As CA') (mk_in As_copy bnf_sets_As CA'))));
           in
             Skip_Proof.prove lthy [] [] goal_in_mono (K (mk_in_mono_tac live))
+            |> Thm.close_derivation
           end;
 
         val in_mono = mk_lazy mk_in_mono;
@@ -881,6 +879,7 @@
                   (HOLogic.mk_eq (mk_in As bnf_sets_As CA', mk_in As_copy bnf_sets_As CA'))));
           in
             Skip_Proof.prove lthy [] [] goal_in_cong (K ((TRY o hyp_subst_tac THEN' rtac refl) 1))
+            |> Thm.close_derivation
           end;
 
         val in_cong = mk_lazy mk_in_cong;
@@ -982,6 +981,7 @@
             Skip_Proof.prove lthy [] [] goal
               (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong axioms)
                 (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_natural'))
+            |> Thm.close_derivation
           end;
 
         val map_wppull = mk_lazy mk_map_wppull;
@@ -997,6 +997,7 @@
               (mk_rel_Gr_tac bnf_rel_def (#map_id axioms) (#map_cong axioms)
                 (#map_wpull axioms) (Lazy.force in_cong) (Lazy.force map_id')
                 (Lazy.force map_comp') (map Lazy.force set_natural'))
+            |> Thm.close_derivation
           end;
 
         val rel_Gr = mk_lazy mk_rel_Gr;
@@ -1013,6 +1014,7 @@
             Skip_Proof.prove lthy [] []
               (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (mono_prems, mono_concl)))
               (mk_rel_mono_tac bnf_rel_def (Lazy.force in_mono))
+            |> Thm.close_derivation
           end;
 
         fun mk_rel_cong () =
@@ -1023,6 +1025,7 @@
             Skip_Proof.prove lthy [] []
               (fold_rev Logic.all (Rs @ Rs_copy) (Logic.list_implies (cong_prems, cong_concl)))
               (fn _ => (TRY o hyp_subst_tac THEN' rtac refl) 1)
+            |> Thm.close_derivation
           end;
 
         val rel_mono = mk_lazy mk_rel_mono;
@@ -1034,6 +1037,7 @@
               (HOLogic.mk_Trueprop
                 (HOLogic.mk_eq (Term.list_comb (relAsAs, map Id_const As'), Id_const CA')))
               (mk_rel_Id_tac live (Lazy.force rel_Gr) (#map_id axioms))
+            |> Thm.close_derivation
           end;
 
         val rel_Id = mk_lazy mk_rel_Id;
@@ -1047,9 +1051,11 @@
             val le_thm = Skip_Proof.prove lthy [] [] le_goal
               (mk_rel_converse_le_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
                 (Lazy.force map_comp') (map Lazy.force set_natural'))
+              |> Thm.close_derivation
             val goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
           in
             Skip_Proof.prove lthy [] [] goal (fn _ => mk_rel_converse_tac le_thm)
+            |> Thm.close_derivation
           end;
 
         val rel_converse = mk_lazy mk_rel_converse;
@@ -1066,6 +1072,7 @@
             Skip_Proof.prove lthy [] [] goal
               (mk_rel_O_tac bnf_rel_def (Lazy.force rel_Id) (#map_cong axioms)
                 (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural'))
+            |> Thm.close_derivation
           end;
 
         val rel_O = mk_lazy mk_rel_O;
@@ -1085,6 +1092,7 @@
               fold_rev Logic.all (x :: y :: Rs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)));
           in
             Skip_Proof.prove lthy [] [] goal (mk_in_rel_tac bnf_rel_def (length bnf_sets))
+            |> Thm.close_derivation
           end;
 
         val in_rel = mk_lazy mk_in_rel;
@@ -1104,48 +1112,55 @@
 
         val bnf = mk_bnf b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs facts
           wits bnf_rel bnf_pred;
-
-        fun note thmN thms =
-          snd o Local_Theory.note
-            ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []), thms);
-
-        fun lazy_note thmN thms = note thmN (map Lazy.force thms);
       in
         (bnf, lthy
           |> (if fact_policy = Note_All_Facts_and_Axioms then
                 let
                   val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits);
+                  val notes =
+                    [(bd_card_orderN, [#bd_card_order axioms]),
+                    (bd_cinfiniteN, [#bd_cinfinite axioms]),
+                    (bd_Card_orderN, [#bd_Card_order facts]),
+                    (bd_CinfiniteN, [#bd_Cinfinite facts]),
+                    (bd_CnotzeroN, [#bd_Cnotzero facts]),
+                    (collect_set_naturalN, [Lazy.force (#collect_set_natural facts)]),
+                    (in_bdN, [#in_bd axioms]),
+                    (in_monoN, [Lazy.force (#in_mono facts)]),
+                    (in_relN, [Lazy.force (#in_rel facts)]),
+                    (map_compN, [#map_comp axioms]),
+                    (map_idN, [#map_id axioms]),
+                    (map_wpullN, [#map_wpull axioms]),
+                    (set_naturalN, #set_natural axioms),
+                    (set_bdN, #set_bd axioms)] @
+                    map2 pair witNs wit_thms
+                    |> map (fn (thmN, thms) =>
+                      ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
+                      [(thms, [])]));
                 in
-                  note bd_card_orderN [#bd_card_order axioms]
-                  #> note bd_cinfiniteN [#bd_cinfinite axioms]
-                  #> note bd_Card_orderN [#bd_Card_order facts]
-                  #> note bd_CinfiniteN [#bd_Cinfinite facts]
-                  #> note bd_CnotzeroN [#bd_Cnotzero facts]
-                  #> lazy_note collect_set_naturalN [#collect_set_natural facts]
-                  #> note in_bdN [#in_bd axioms]
-                  #> lazy_note in_monoN [#in_mono facts]
-                  #> lazy_note in_relN [#in_rel facts]
-                  #> note map_compN [#map_comp axioms]
-                  #> note map_idN [#map_id axioms]
-                  #> note map_wpullN [#map_wpull axioms]
-                  #> note set_naturalN (#set_natural axioms)
-                  #> note set_bdN (#set_bd axioms)
-                  #> fold2 note witNs wit_thms
+                  Local_Theory.notes notes #> snd
                 end
               else
                 I)
           |> (if fact_policy = Note_All_Facts_and_Axioms orelse
                  fact_policy = Derive_All_Facts_Note_Most then
-                lazy_note rel_IdN [#rel_Id facts]
-                #> lazy_note rel_GrN [#rel_Gr facts]
-                #> lazy_note rel_converseN [#rel_converse facts]
-                #> lazy_note rel_ON [#rel_O facts]
-                #> lazy_note map_id'N [#map_id' facts]
-                #> lazy_note map_comp'N [#map_comp' facts]
-                #> note map_congN [#map_cong axioms]
-                #> lazy_note set_natural'N (#set_natural' facts)
-                #> Local_Theory.declaration {syntax = false, pervasive = true}
-                  (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf)))
+                let
+                  val notes =
+                    [(map_congN, [#map_cong axioms]),
+                    (rel_IdN, [Lazy.force (#rel_Id facts)]),
+                    (rel_GrN, [Lazy.force (#rel_Gr facts)]),
+                    (rel_converseN, [Lazy.force (#rel_converse facts)]),
+                    (rel_ON, [Lazy.force (#rel_O facts)]),
+                    (map_id'N, [Lazy.force (#map_id' facts)]),
+                    (map_comp'N, [Lazy.force (#map_comp' facts)]),
+                    (set_natural'N, map Lazy.force (#set_natural' facts))]
+                    |> map (fn (thmN, thms) =>
+                      ((qualify (Binding.qualify true (Binding.name_of b) (Binding.name thmN)), []),
+                      [(thms, [])]));
+                in
+                  Local_Theory.notes notes #> snd
+                  #> Local_Theory.declaration {syntax = false, pervasive = true}
+                    (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf)))
+                end
               else
                 I))
       end;
@@ -1163,9 +1178,10 @@
       Skip_Proof.prove lthy [] [] wit_goal wits_tac
       |> Conjunction.elim_balanced (length wit_goals)
       |> map2 (Conjunction.elim_balanced o length) wit_goalss
-      |> map (map (Thm.forall_elim_vars 0));
+      |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0))
   in
-    (map2 (Skip_Proof.prove lthy [] []) goals (map (unfold_defs_tac lthy defs) tacs))
+    (map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
+      goals (map (unfold_defs_tac lthy defs) tacs))
     |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
   end) oo prepare_def const_policy fact_policy qualify
   (fn ctxt => singleton (Type_Infer_Context.infer_types ctxt)) Ds;
diff -r 61e222517d06 -r 0e5b859e1c91 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 00:16:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Tue Sep 04 12:10:19 2012 +0200
@@ -62,11 +62,6 @@
     val ls = 1 upto m;
     val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
 
-    fun note thmN thms = snd o Local_Theory.note
-      ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
-    fun notes thmN thmss = fold2 (fn b => fn thms => snd o Local_Theory.note
-      ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms)) bs thmss;
-
     (* TODO: check if m, n etc are sane *)
 
     val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
@@ -243,6 +238,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
           (K (mk_map_comp_id_tac map_comp))
+        |> Thm.close_derivation
       end;
 
     val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's;
@@ -261,6 +257,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
           (K (mk_map_congL_tac m map_cong map_id'))
+        |> Thm.close_derivation
       end;
 
     val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
@@ -281,7 +278,7 @@
           prems concls xFs xFs_copy;
       in
         map (fn goal => Skip_Proof.prove lthy [] [] goal
-          (K ((hyp_subst_tac THEN' rtac refl) 1))) goals
+          (K ((hyp_subst_tac THEN' rtac refl) 1)) |> Thm.close_derivation) goals
       end;
 
     val timer = time (timer "Derived simple theorems");
@@ -344,7 +341,7 @@
             (Logic.list_implies (coalg_prem :: [prem], concl))) concls) zs prems conclss;
       in
         map (fn goals => map (fn goal => Skip_Proof.prove lthy [] [] goal
-          (K (mk_coalg_set_tac coalg_def))) goals) goalss
+          (K (mk_coalg_set_tac coalg_def)) |> Thm.close_derivation) goals) goalss
       end;
 
     val coalg_set_thmss' = transpose coalg_set_thmss;
@@ -360,6 +357,7 @@
           (K (stac coalg_def 1 THEN CONJ_WRAP
             (K (EVERY' [rtac ballI, rtac CollectI,
               CONJ_WRAP' (K (EVERY' [rtac @{thm subset_UNIV}])) allAs] 1)) ss))
+        |> Thm.close_derivation
       end;
 
     val timer = time (timer "Coalgebra definition & thms");
@@ -424,7 +422,8 @@
                (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 =
-          Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def));
+          Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def))
+          |> Thm.close_derivation;
       in
         (map prove image_goals, map prove elim_goals)
       end;
@@ -439,6 +438,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
           (K (mk_mor_incl_tac mor_def map_id's))
+        |> Thm.close_derivation
       end;
 
     val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);
@@ -455,6 +455,7 @@
           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
             (Logic.list_implies (prems, concl)))
           (K (mk_mor_comp_tac mor_def mor_image'_thms morE_thms map_comp_id_thms))
+        |> Thm.close_derivation
       end;
 
     val mor_cong_thm =
@@ -467,6 +468,7 @@
           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
             (Logic.list_implies (prems, concl)))
           (K ((hyp_subst_tac THEN' atac) 1))
+        |> Thm.close_derivation
       end;
 
     val mor_UNIV_thm =
@@ -480,6 +482,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
           (K (mk_mor_UNIV_tac morE_thms mor_def))
+        |> Thm.close_derivation
       end;
 
     val mor_str_thm =
@@ -491,6 +494,7 @@
           (fold_rev Logic.all 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
       end;
 
     val mor_sum_case_thm =
@@ -503,6 +507,7 @@
           (fold_rev Logic.all (s's @ sum_ss) (HOLogic.mk_Trueprop
             (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls)))
           (K (mk_mor_sum_case_tac ks mor_UNIV_thm))
+        |> Thm.close_derivation
       end;
 
     val timer = time (timer "Morphism definition & thms");
@@ -634,15 +639,16 @@
       in
         (map3 (fn goals => fn defs => fn rec_Sucs =>
           map3 (fn goal => fn def => fn rec_Suc =>
-            Skip_Proof.prove lthy [] [] goal
-              (K (mk_set_incl_hset_tac def rec_Suc)))
+            Skip_Proof.prove lthy [] [] goal (K (mk_set_incl_hset_tac def rec_Suc))
+            |> Thm.close_derivation)
           goals defs rec_Sucs)
         set_incl_hset_goalss hset_defss hset_rec_Sucss,
         map3 (fn goalss => fn defsi => fn rec_Sucs =>
           map3 (fn k => fn goals => fn defsk =>
             map4 (fn goal => fn defk => fn defi => fn rec_Suc =>
               Skip_Proof.prove lthy [] [] goal
-                (K (mk_set_hset_incl_hset_tac n [defk, defi] rec_Suc k)))
+                (K (mk_set_hset_incl_hset_tac n [defk, defi] rec_Suc k))
+              |> Thm.close_derivation)
             goals defsk defsi rec_Sucs)
           ks goalss hset_defss)
         set_hset_incl_hset_goalsss hset_defss hset_rec_Sucss)
@@ -671,7 +677,8 @@
           ss zs setssAs hsetssAs;
       in
         map2 (map2 (fn goal => fn thms =>
-          Skip_Proof.prove lthy [] [] goal (K (mk_set_incl_hin_tac thms))))
+          Skip_Proof.prove lthy [] [] goal (K (mk_set_incl_hin_tac thms))
+          |> Thm.close_derivation))
         set_incl_hin_goalss set_hset_incl_hset_thmsss
       end;
 
@@ -707,7 +714,8 @@
             map4 (fn goal => fn cts => fn hset_rec_0s => fn hset_rec_Sucs =>
               singleton (Proof_Context.export names_lthy lthy)
                 (Skip_Proof.prove lthy [] [] goal
-                  (mk_hset_rec_minimal_tac m cts hset_rec_0s hset_rec_Sucs)))
+                  (mk_hset_rec_minimal_tac m cts hset_rec_0s hset_rec_Sucs))
+              |> Thm.close_derivation)
             goals ctss hset_rec_0ss' hset_rec_Sucss'
           end;
 
@@ -721,7 +729,8 @@
       in
         map3 (fn goal => fn hset_defs => fn hset_rec_minimal =>
           Skip_Proof.prove lthy [] [] goal
-            (mk_hset_minimal_tac n hset_defs hset_rec_minimal))
+            (mk_hset_minimal_tac n hset_defs hset_rec_minimal)
+          |> Thm.close_derivation)
         goals hset_defss' hset_rec_minimal_thms
       end;
 
@@ -747,7 +756,8 @@
               singleton (Proof_Context.export names_lthy lthy)
                 (Skip_Proof.prove lthy [] [] goal
                   (K (mk_mor_hset_rec_tac m n cts j hset_rec_0s hset_rec_Sucs
-                    morE_thms set_natural'ss coalg_set_thmss))))
+                    morE_thms set_natural'ss coalg_set_thmss)))
+              |> Thm.close_derivation)
             ls goals ctss hset_rec_0ss' hset_rec_Sucss'
           end;
 
@@ -766,7 +776,8 @@
       in
         map3 (map3 (fn goal => fn hset_def => fn mor_hset_rec =>
           Skip_Proof.prove lthy [] [] goal
-            (K (mk_mor_hset_tac hset_def mor_hset_rec))))
+            (K (mk_mor_hset_tac hset_def mor_hset_rec))
+          |> Thm.close_derivation))
         goalss hset_defss' mor_hset_rec_thmss
       end;
 
@@ -832,6 +843,7 @@
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
             (Logic.list_implies (prems, concl)))
           (K ((hyp_subst_tac THEN' atac) 1))
+        |> Thm.close_derivation
       end;
 
     val bis_rel_thm =
@@ -850,6 +862,7 @@
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
             (HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_bis As Bs ss B's s's Rs, rhs))))
           (K (mk_bis_rel_tac m bis_def rel_defs map_comp's map_congs set_natural'ss))
+        |> Thm.close_derivation
       end;
 
     val bis_converse_thm =
@@ -858,7 +871,8 @@
           (Logic.mk_implies
             (HOLogic.mk_Trueprop (mk_bis As Bs ss B's s's Rs),
             HOLogic.mk_Trueprop (mk_bis As B's s's Bs ss (map mk_converse Rs)))))
-      (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converses));
+        (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converses))
+      |> Thm.close_derivation;
 
     val bis_O_thm =
       let
@@ -872,6 +886,7 @@
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ B''s @ s''s @ Rs @ R's)
             (Logic.list_implies (prems, concl)))
           (K (mk_bis_O_tac m bis_rel_thm rel_congs rel_Os))
+        |> Thm.close_derivation
       end;
 
     val bis_Gr_thm =
@@ -883,6 +898,7 @@
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ fs)
             (Logic.list_implies ([coalg_prem, mor_prem], concl)))
           (mk_bis_Gr_tac bis_rel_thm rel_Grs mor_image_thms morE_thms coalg_in_thms)
+        |> Thm.close_derivation
       end;
 
     val bis_image2_thm = bis_cong_thm OF
@@ -904,6 +920,7 @@
           (fold_rev Logic.all (Idx :: As @ Bs @ ss @ B's @ s's @ Ris)
             (Logic.mk_implies (prem, concl)))
           (mk_bis_Union_tac bis_def in_mono'_thms)
+        |> Thm.close_derivation
       end;
 
     (* self-bisimulation *)
@@ -959,7 +976,8 @@
       Skip_Proof.prove lthy [] []
         (fold_rev Logic.all (As @ Bs @ ss)
           (HOLogic.mk_Trueprop (mk_sbis As Bs ss (map (mk_lsbis As Bs ss) ks))))
-        (K (mk_sbis_lsbis_tac lsbis_defs bis_Union_thm bis_cong_thm));
+        (K (mk_sbis_lsbis_tac lsbis_defs bis_Union_thm bis_cong_thm))
+      |> Thm.close_derivation;
 
     val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
       (bis_def RS @{thm subst[of _ _ "%x. x"]} RS conjunct1 RS mk_conjunctN n i)) ks;
@@ -973,7 +991,7 @@
           (Logic.mk_implies (sbis_prem, mk_concl i R))) ks sRs;
       in
         map3 (fn goal => fn i => fn def => Skip_Proof.prove lthy [] [] goal
-          (K (mk_incl_lsbis_tac n i def))) goals ks lsbis_defs
+          (K (mk_incl_lsbis_tac n i def)) |> Thm.close_derivation) goals ks lsbis_defs
       end;
 
     val equiv_lsbis_thms =
@@ -985,7 +1003,8 @@
         map3 (fn goal => fn l_incl => fn incl_l =>
           Skip_Proof.prove lthy [] [] goal
             (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l
-              bis_diag_thm bis_converse_thm bis_O_thm)))
+              bis_diag_thm bis_converse_thm bis_O_thm))
+          |> Thm.close_derivation)
         goals lsbis_incl_thms incl_lsbis_thms
       end;
 
@@ -1269,7 +1288,8 @@
     val coalgT_thm =
       Skip_Proof.prove lthy [] []
         (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_coalg As carTAs strTAs)))
-        (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_natural'ss);
+        (mk_coalgT_tac m (coalg_def :: isNode_defs @ carT_defs) strT_defs set_natural'ss)
+      |> Thm.close_derivation;
 
     val card_of_carT_thms =
       let
@@ -1285,6 +1305,7 @@
             (fold_rev Logic.all As (HOLogic.mk_Trueprop (mk_ordLeq lhs rhs)))
             (K (mk_card_of_carT_tac m isNode_defs sbd_sbd_thm
               sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds))
+          |> Thm.close_derivation
       in
         map (fn def => @{thm ordLeq_transitive[OF
           card_of_mono1[OF ord_eq_le_trans[OF _ Collect_restrict']]]} OF [def, card_of_carT])
@@ -1310,7 +1331,8 @@
             fn carT_def => fn strT_def => fn isNode_def => fn set_naturals =>
           map2 (fn goal => fn set_natural =>
             Skip_Proof.prove lthy [] [] goal
-            (mk_carT_set_tac n i carT_def strT_def isNode_def set_natural))
+              (mk_carT_set_tac n i carT_def strT_def isNode_def set_natural)
+            |> Thm.close_derivation)
           goals (drop m set_naturals))
         ks goalss carT_defs strT_defs isNode_defs set_natural'ss
       end;
@@ -1354,7 +1376,8 @@
                       (K (mk_strT_hset_tac n m j arg_cong_cTs cTs cts
                         carT_defs strT_defs isNode_defs
                         set_incl_hsets set_hset_incl_hsetss coalg_set_thmss' carT_set_thmss'
-                        coalgT_thm set_natural'ss))))
+                        coalgT_thm set_natural'ss)))
+                  |> Thm.close_derivation)
                 ls goals ctss set_incl_hset_thmss' set_hset_incl_hset_thmsss''
               end;
 
@@ -1375,9 +1398,10 @@
         map5 (fn carT_prem => fn isNode_prems => fn in_prem => fn concls => fn strT_hset_thmss =>
           map4 (fn isNode_prem => fn concl => fn isNode_def => fn strT_hset_thms =>
             Skip_Proof.prove lthy [] []
-            (fold_rev Logic.all (Kl :: lab :: kl :: As @ As_copy)
-              (Logic.list_implies ([carT_prem, prem, isNode_prem, in_prem], concl)))
-            (mk_isNode_hset_tac n isNode_def strT_hset_thms))
+              (fold_rev Logic.all (Kl :: lab :: kl :: As @ As_copy)
+                (Logic.list_implies ([carT_prem, prem, isNode_prem, in_prem], concl)))
+              (mk_isNode_hset_tac n isNode_def strT_hset_thms)
+            |> Thm.close_derivation)
           isNode_prems concls isNode_defs
           (if m = 0 then replicate n [] else transpose strT_hset_thmss))
         carT_prems isNode_premss in_prems conclss
@@ -1556,7 +1580,8 @@
 
         val Lev_sbd = singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbd_thmss)));
+            (K (mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbd_thmss))
+          |> Thm.close_derivation);
 
         val Lev_sbd' = mk_specN n Lev_sbd;
       in
@@ -1574,7 +1599,8 @@
 
         val length_Lev = singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_length_Lev_tac cts Lev_0s Lev_Sucs)));
+            (K (mk_length_Lev_tac cts Lev_0s Lev_Sucs))
+          |> Thm.close_derivation);
 
         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;
@@ -1585,8 +1611,8 @@
         val goals = map2 mk_goal ks zs;
 
         val length_Levs' = map2 (fn goal => fn length_Lev =>
-          Skip_Proof.prove lthy [] [] goal
-            (K (mk_length_Lev'_tac length_Lev))) goals length_Levs;
+          Skip_Proof.prove lthy [] [] goal (K (mk_length_Lev'_tac length_Lev))
+          |> Thm.close_derivation) goals length_Levs;
       in
         (length_Levs, length_Levs')
       end;
@@ -1603,7 +1629,8 @@
 
         val prefCl_Lev = singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs)));
+            (K (mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs)))
+          |> Thm.close_derivation;
 
         val prefCl_Lev' = mk_specN (n + 2) prefCl_Lev;
       in
@@ -1626,7 +1653,8 @@
 
         val rv_last = singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss)));
+            (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss)))
+          |> Thm.close_derivation;
 
         val rv_last' = mk_specN (n + 1) rv_last;
       in
@@ -1651,7 +1679,8 @@
           (Skip_Proof.prove lthy [] []
             (Logic.mk_implies (coalg_prem, HOLogic.mk_Trueprop goal))
             (K (mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss
-              coalg_set_thmss from_to_sbd_thmss)));
+              coalg_set_thmss from_to_sbd_thmss)))
+          |> Thm.close_derivation;
 
         val set_rv_Lev' = mk_specN (n + 1) set_rv_Lev;
       in
@@ -1689,7 +1718,8 @@
 
         val set_Lev = singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)));
+            (K (mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)))
+          |> Thm.close_derivation;
 
         val set_Lev' = mk_specN (3 * n + 1) set_Lev;
       in
@@ -1727,7 +1757,8 @@
         val set_image_Lev = singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
             (K (mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss
-              from_to_sbd_thmss to_sbd_inj_thmss)));
+              from_to_sbd_thmss to_sbd_inj_thmss)))
+          |> Thm.close_derivation;
 
         val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev;
       in
@@ -1746,7 +1777,8 @@
           to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
           length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
           set_rv_Lev_thmsss set_Lev_thmsss set_image_Lev_thmsss
-          set_natural'ss coalg_set_thmss map_comp_id_thms map_congs map_arg_cong_thms);
+          set_natural'ss coalg_set_thmss map_comp_id_thms map_congs map_arg_cong_thms)
+      |> Thm.close_derivation;
 
     val timer = time (timer "Behavioral morphism");
 
@@ -1776,19 +1808,22 @@
       in
         map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong =>
           Skip_Proof.prove lthy [] [] goal
-            (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBIS_thms)))
+            (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBIS_thms))
+          |> Thm.close_derivation)
         goals lsbisE_thms map_comp_id_thms map_congs
       end;
 
     val coalg_final_thm = Skip_Proof.prove lthy [] [] (fold_rev Logic.all As
       (HOLogic.mk_Trueprop (mk_coalg As car_finalAs str_finalAs)))
       (K (mk_coalg_final_tac m coalg_def congruent_str_final_thms equiv_LSBIS_thms
-        set_natural'ss coalgT_set_thmss));
+        set_natural'ss coalgT_set_thmss))
+      |> Thm.close_derivation;
 
     val mor_T_final_thm = Skip_Proof.prove lthy [] [] (fold_rev Logic.all As
       (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finalAs str_finalAs
         (map (mk_proj o mk_LSBIS As) ks))))
-      (K (mk_mor_T_final_tac mor_def congruent_str_final_thms equiv_LSBIS_thms));
+      (K (mk_mor_T_final_tac mor_def congruent_str_final_thms equiv_LSBIS_thms))
+      |> Thm.close_derivation;
 
     val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
     val in_car_final_thms = map (fn mor_image' => mor_image' OF
@@ -1892,12 +1927,14 @@
           Skip_Proof.prove lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs unfs car_finals str_finals Rep_Ts))
             (mk_mor_Rep_tac m (mor_def :: unf_defs) Reps Abs_inverses coalg_final_set_thmss
-              map_comp_id_thms map_congL_thms);
+              map_comp_id_thms map_congL_thms)
+          |> Thm.close_derivation;
 
         val mor_Abs =
           Skip_Proof.prove lthy [] []
             (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs unfs Abs_Ts))
-            (mk_mor_Abs_tac (mor_def :: unf_defs) Abs_inverses);
+            (mk_mor_Abs_tac (mor_def :: unf_defs) Abs_inverses)
+          |> Thm.close_derivation;
       in
         (mor_Rep, mor_Abs)
       end;
@@ -1946,6 +1983,7 @@
             (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs unfs (map (mk_coiter Ts ss) ks))))
           (K (mk_mor_coiter_tac m mor_UNIV_thm unf_defs coiter_defs Abs_inverses' morEs'
             map_comp_id_thms map_congs))
+        |> Thm.close_derivation
       end;
     val coiter_thms = map (fn thm => (thm OF [mor_coiter_thm, UNIV_I]) RS sym) morE_thms;
 
@@ -1959,7 +1997,8 @@
         `split_conj_thm (Skip_Proof.prove lthy [] [] goal
           (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)))
+            lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects))
+          |> Thm.close_derivation)
       end;
 
     val unique_mor_thms =
@@ -1975,7 +2014,8 @@
         val unique_mor = Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (Bs @ ss @ coiter_fs @ coiter_fs_copy @ zs)
             (Logic.list_implies (prems, unique)))
-          (K (mk_unique_mor_tac raw_coind_thms bis_image2_thm));
+          (K (mk_unique_mor_tac raw_coind_thms bis_image2_thm))
+          |> Thm.close_derivation;
       in
         map (fn thm => conjI RSN (2, thm RS mp)) (split_conj_thm unique_mor)
       end;
@@ -1992,7 +2032,8 @@
 
         val unique_mor = Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (ss @ coiter_fs) (Logic.mk_implies (prem, unique)))
-          (K (mk_coiter_unique_mor_tac raw_coind_thms bis_thm mor_thm coiter_defs));
+          (K (mk_coiter_unique_mor_tac raw_coind_thms bis_thm mor_thm coiter_defs))
+          |> Thm.close_derivation;
       in
         `split_conj_thm unique_mor
       end;
@@ -2054,7 +2095,8 @@
       in
         map5 (fn goal => fn fld_def => fn coiter => fn map_comp_id => fn map_congL =>
           Skip_Proof.prove lthy [] [] goal
-            (mk_unf_o_fld_tac fld_def coiter map_comp_id map_congL coiter_o_unf_thms))
+            (mk_unf_o_fld_tac fld_def coiter map_comp_id map_congL coiter_o_unf_thms)
+          |> Thm.close_derivation)
           goals fld_defs coiter_thms map_comp_id_thms map_congL_thms
       end;
 
@@ -2139,8 +2181,9 @@
       in
         map3 (fn goal => fn coiter => fn map_cong =>
           Skip_Proof.prove lthy [] [] goal
-            (mk_corec_tac m corec_defs coiter map_cong corec_Inl_sum_thms))
-          goals coiter_thms map_congs
+            (mk_corec_tac m corec_defs coiter map_cong corec_Inl_sum_thms)
+          |> Thm.close_derivation)
+        goals coiter_thms map_congs
       end;
 
     val timer = time (timer "corec definitions & thms");
@@ -2185,7 +2228,8 @@
 
         val rel_coinduct = Local_Defs.unfold lthy @{thms diag_UNIV}
           (Skip_Proof.prove lthy [] [] rel_coinduct_goal
-            (K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm)));
+            (K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm))
+          |> Thm.close_derivation);
 
         fun mk_unf_prem upto_eq phi unf map_nth sets Jz Jz_copy FJz =
           let
@@ -2216,7 +2260,8 @@
 
         val unf_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (unf_prems, concl));
         val unf_coinduct = Skip_Proof.prove lthy [] [] unf_coinduct_goal
-          (K (mk_unf_coinduct_tac m ks raw_coind_thm bis_def));
+          (K (mk_unf_coinduct_tac m ks raw_coind_thm bis_def))
+          |> Thm.close_derivation;
 
         val cTs = map (SOME o certifyT lthy o TFree) coinduct_params;
         val cts = map3 (SOME o certify lthy ooo mk_phi true) phis Jzs1 Jzs2;
@@ -2224,13 +2269,15 @@
         val rel_coinduct_upto = singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] []
             (fold_rev Logic.all zs (Logic.list_implies (rel_upto_prems, concl)))
-            (K (mk_rel_coinduct_upto_tac m cTs cts rel_coinduct rel_monos rel_Ids)));
+            (K (mk_rel_coinduct_upto_tac m cTs cts rel_coinduct rel_monos rel_Ids)))
+          |> Thm.close_derivation;
 
         val unf_coinduct_upto = singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] []
             (fold_rev Logic.all zs (Logic.list_implies (unf_upto_prems, concl)))
             (K (mk_unf_coinduct_upto_tac ks cTs cts unf_coinduct bis_def
-              (tcoalg_thm RS bis_diag_thm))));
+              (tcoalg_thm RS bis_diag_thm))))
+          |> Thm.close_derivation;
 
         val pred_coinduct = rel_coinduct
           |> Local_Defs.unfold lthy @{thms Id_def'}
@@ -2338,9 +2385,11 @@
                 HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), unf))));
             val goals = map4 mk_goal fs_maps map_FTFT's unfs unf's;
             val cTs = map (SOME o certifyT lthy) FTs';
-            val maps = map5 (fn goal => fn cT => fn coiter => fn map_comp' => fn map_cong =>
-              Skip_Proof.prove lthy [] [] goal
-                (K (mk_map_tac m n cT coiter map_comp' map_cong)))
+            val maps =
+              map5 (fn goal => fn cT => fn coiter => fn map_comp' => fn map_cong =>
+                Skip_Proof.prove lthy [] [] goal
+                  (K (mk_map_tac m n cT coiter map_comp' map_cong))
+                |> Thm.close_derivation)
               goals cTs coiter_thms map_comp's map_congs;
           in
             map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
@@ -2355,7 +2404,8 @@
                 fs_maps gs_maps fgs_maps)))
           in
             split_conj_thm (Skip_Proof.prove lthy [] [] goal
-              (K (mk_map_comp_tac m n map_thms map_comps map_congs coiter_unique_thm)))
+              (K (mk_map_comp_tac m n map_thms map_comps map_congs coiter_unique_thm))
+              |> Thm.close_derivation)
           end;
 
         val (map_unique_thms, map_unique_thm) =
@@ -2369,7 +2419,8 @@
                 (map2 (curry HOLogic.mk_eq) us fs_maps));
             val unique = Skip_Proof.prove lthy [] []
               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
-              (mk_map_unique_tac coiter_unique_thm map_comps);
+              (mk_map_unique_tac coiter_unique_thm map_comps)
+              |> Thm.close_derivation;
           in
             `split_conj_thm unique
           end;
@@ -2408,7 +2459,8 @@
             val set_le_thmss = map split_conj_thm
               (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss =>
                 Skip_Proof.prove lthy [] [] goal
-                  (K (mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss)))
+                  (K (mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss))
+                |> Thm.close_derivation)
               le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss');
 
             val simp_goalss = map (map2 (fn z => fn goal =>
@@ -2417,7 +2469,8 @@
           in
             map4 (map4 (fn goal => fn set_le => fn set_incl_hset => fn set_hset_incl_hsets =>
               Skip_Proof.prove lthy [] [] goal
-                (K (mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets))))
+                (K (mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets))
+              |> Thm.close_derivation))
             simp_goalss set_le_thmss set_incl_hset_thmss' set_hset_incl_hset_thmsss'
           end;
 
@@ -2443,10 +2496,12 @@
             val ctss =
               map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
 
-            val thms = map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
-              singleton (Proof_Context.export names_lthy lthy)
-                (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
-                  (mk_col_natural_tac cts rec_0s rec_Sucs map_simp_thms set_natural'ss)))
+            val thms =
+              map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
+                singleton (Proof_Context.export names_lthy lthy)
+                  (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
+                    (mk_col_natural_tac cts rec_0s rec_Sucs map_simp_thms set_natural'ss))
+                |> Thm.close_derivation)
               goals ctss hset_rec_0ss' hset_rec_Sucss';
           in
             map (split_conj_thm o mk_specN n) thms
@@ -2464,11 +2519,13 @@
             val ctss =
               map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
 
-            val thms = map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
-              singleton (Proof_Context.export names_lthy lthy)
-                (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
-                  (K (mk_col_bd_tac m j cts rec_0s rec_Sucs
-                    sbd_Card_order sbd_Cinfinite set_sbdss))))
+            val thms =
+              map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
+                singleton (Proof_Context.export names_lthy lthy)
+                  (Skip_Proof.prove lthy [] [] (HOLogic.mk_Trueprop goal)
+                    (K (mk_col_bd_tac m j cts rec_0s rec_Sucs
+                      sbd_Card_order sbd_Cinfinite set_sbdss)))
+                |> Thm.close_derivation)
               ls goals ctss hset_rec_0ss' hset_rec_Sucss';
           in
             map (split_conj_thm o mk_specN n) thms
@@ -2513,6 +2570,7 @@
               (Skip_Proof.prove lthy [] [] goal
               (K (mk_mcong_tac m (rtac coinduct) map_comp's map_simp_thms map_congs set_natural'ss
               set_hset_thmss set_hset_hset_thmsss)))
+              |> Thm.close_derivation
           in
             split_conj_thm thm
           end;
@@ -2547,6 +2605,7 @@
           in
             Skip_Proof.prove lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms
               set_natural'ss pickWP_assms_tacs)
+            |> Thm.close_derivation
           end;
 
         val (mor_thePull_fst_thm, mor_thePull_snd_thm, mor_thePull_pick_thm) =
@@ -2569,11 +2628,11 @@
               (Logic.mk_implies (wpull_prem, mor_pick));
           in
             (Skip_Proof.prove lthy [] [] goal_fst (mk_mor_thePull_fst_tac m mor_def map_wpull_thms
-              map_comp's pickWP_assms_tacs),
+              map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
             Skip_Proof.prove lthy [] [] goal_snd (mk_mor_thePull_snd_tac m mor_def map_wpull_thms
-              map_comp's pickWP_assms_tacs),
+              map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
             Skip_Proof.prove lthy [] [] goal_pick (mk_mor_thePull_pick_tac mor_def coiter_thms
-              map_comp's))
+              map_comp's) |> Thm.close_derivation)
           end;
 
         val pick_col_thmss =
@@ -2593,10 +2652,12 @@
             val goals =
               map (fn concl => Logic.mk_implies (wpull_prem, HOLogic.mk_Trueprop concl)) concls;
 
-            val thms = map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
-              singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal
-                (mk_pick_col_tac m j cts rec_0s rec_Sucs coiter_thms set_natural'ss map_wpull_thms
-                  pickWP_assms_tacs)))
+            val thms =
+              map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
+                singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal
+                  (mk_pick_col_tac m j cts rec_0s rec_Sucs coiter_thms set_natural'ss map_wpull_thms
+                    pickWP_assms_tacs))
+                |> Thm.close_derivation)
               ls goals ctss hset_rec_0ss' hset_rec_Sucss';
           in
             map (map (fn thm => thm RS mp) o split_conj_thm o mk_specN n) thms
@@ -2785,7 +2846,8 @@
           in
             map2 (fn goal => fn induct =>
               Skip_Proof.prove lthy [] [] goal
-               (mk_coind_wit_tac induct coiter_thms (flat set_natural'ss) wit_thms))
+                (mk_coind_wit_tac induct coiter_thms (flat set_natural'ss) wit_thms)
+              |> Thm.close_derivation)
             goals hset_induct_thms
             |> map split_conj_thm
             |> transpose
@@ -2861,8 +2923,9 @@
               fn map_simp => fn set_simps => fn unf_inject => fn unf_fld =>
               fn set_naturals => fn set_incls => fn set_set_inclss =>
               Skip_Proof.prove lthy [] [] goal
-               (K (mk_rel_unfold_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps
-                 unf_inject unf_fld set_naturals set_incls set_set_inclss)))
+                (K (mk_rel_unfold_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps
+                  unf_inject unf_fld set_naturals set_incls set_set_inclss))
+              |> Thm.close_derivation)
             ks goals in_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
               unf_inject_thms unf_fld_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
           end;
@@ -2875,42 +2938,64 @@
             val goals = map6 mk_goal Jzs Jz's unfs unf's Jpredphis predphis;
           in
             map3 (fn goal => fn pred_def => fn Jrel_unfold =>
-              Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Jpred_defs Jrel_unfold))
+              Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Jpred_defs Jrel_unfold)
+              |> Thm.close_derivation)
             goals pred_defs Jrel_unfold_thms
           end;
 
         val timer = time (timer "additional properties");
 
         val ls' = if m = 1 then [0] else ls;
+
+        val Jbnf_common_notes =
+          [(map_uniqueN, [fold_maps map_unique_thm])] @
+          map2 (fn i => fn thm => (mk_set_inductN i, [thm])) ls' set_induct_thms
+          |> map (fn (thmN, thms) =>
+            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
+
+        val Jbnf_notes =
+          [(map_simpsN, map single folded_map_simp_thms),
+          (set_inclN, set_incl_thmss),
+          (set_set_inclN, map flat set_set_incl_thmsss), (* nicer names? *)
+          (rel_unfoldN, map single Jrel_unfold_thms),
+          (pred_unfoldN, map single Jpred_unfold_thms)] @
+          map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
+          |> maps (fn (thmN, thmss) =>
+            map2 (fn b => fn thms =>
+              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
+            bs thmss)
       in
-        lthy
-        |> note map_uniqueN [fold_maps map_unique_thm]
-        |> notes map_simpsN (map single folded_map_simp_thms)
-        |> fold2 (fn i => notes (mk_set_simpsN i) o map single) ls' folded_set_simp_thmss
-        |> notes set_inclN set_incl_thmss
-        |> notes set_set_inclN (map flat set_set_incl_thmsss) (* nicer names? *)
-        |> fold2 (fn i => note (mk_set_inductN i) o single) ls' set_induct_thms
-        |> notes rel_unfoldN (map single Jrel_unfold_thms)
-        |> notes pred_unfoldN (map single Jpred_unfold_thms)
+        lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd
       end;
+
+      val common_notes =
+        [(unf_coinductN, [unf_coinduct_thm]),
+        (rel_coinductN, [rel_coinduct_thm]),
+        (pred_coinductN, [pred_coinduct_thm]),
+        (unf_coinduct_uptoN, [unf_coinduct_upto_thm]),
+        (rel_coinduct_uptoN, [rel_coinduct_upto_thm]),
+        (pred_coinduct_uptoN, [pred_coinduct_upto_thm])]
+        |> map (fn (thmN, thms) =>
+          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
+
+      val notes =
+        [(coiterN, coiter_thms),
+        (coiter_uniqueN, coiter_unique_thms),
+        (corecN, corec_thms),
+        (unf_fldN, unf_fld_thms),
+        (fld_unfN, fld_unf_thms),
+        (unf_injectN, unf_inject_thms),
+        (unf_exhaustN, unf_exhaust_thms),
+        (fld_injectN, fld_inject_thms),
+        (fld_exhaustN, fld_exhaust_thms),
+        (fld_coiterN, fld_coiter_thms)]
+        |> map (apsnd (map single))
+        |> maps (fn (thmN, thmss) =>
+          map2 (fn b => fn thms =>
+            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
+          bs thmss)
   in
-    lthy
-    |> notes coiterN (map single coiter_thms)
-    |> notes coiter_uniqueN (map single coiter_unique_thms)
-    |> notes corecN (map single corec_thms)
-    |> notes unf_fldN (map single unf_fld_thms)
-    |> notes fld_unfN (map single fld_unf_thms)
-    |> notes unf_injectN (map single unf_inject_thms)
-    |> notes unf_exhaustN (map single unf_exhaust_thms)
-    |> notes fld_injectN (map single fld_inject_thms)
-    |> notes fld_exhaustN (map single fld_exhaust_thms)
-    |> notes fld_coiterN (map single fld_coiter_thms)
-    |> note unf_coinductN [unf_coinduct_thm]
-    |> note rel_coinductN [rel_coinduct_thm]
-    |> note pred_coinductN [pred_coinduct_thm]
-    |> note unf_coinduct_uptoN [unf_coinduct_upto_thm]
-    |> note rel_coinduct_uptoN [rel_coinduct_upto_thm]
-    |> note pred_coinduct_uptoN [pred_coinduct_upto_thm]
+    lthy |> Local_Theory.notes (common_notes @ notes) |> snd
   end;
 
 val _ =
diff -r 61e222517d06 -r 0e5b859e1c91 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 00:16:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 04 12:10:19 2012 +0200
@@ -31,11 +31,6 @@
     val m = live - n (*passive, if 0 don't generate a new bnf*)
     val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
 
-    fun note thmN thms = snd o Local_Theory.note
-      ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms);
-    fun notes thmN thmss = fold2 (fn b => fn thms => snd o Local_Theory.note
-      ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), thms)) bs thmss;
-
     (* TODO: check if m, n etc are sane *)
 
     val Dss = map (fn Ds => map TFree (fold Term.add_tfreesT Ds [])) Dss_insts;
@@ -176,6 +171,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (x :: fs @ all_gs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
           (K (mk_map_comp_id_tac map_comp))
+        |> Thm.close_derivation
       end;
 
     val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's;
@@ -193,6 +189,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
           (K (mk_map_congL_tac m map_cong map_id'))
+        |> Thm.close_derivation
       end;
 
     val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
@@ -252,8 +249,9 @@
           fold_rev Logic.all (x :: As @ Bs @ ss)
             (Logic.list_implies (alg_prem :: prems, concl))) xFs premss concls;
       in
-        map (fn goal => Skip_Proof.prove lthy [] [] goal
-          (K (mk_alg_set_tac alg_def))) goals
+        map (fn goal =>
+          Skip_Proof.prove lthy [] [] goal (K (mk_alg_set_tac alg_def)) |> Thm.close_derivation)
+        goals
       end;
 
     fun mk_talg ATs BTs = mk_alg (map HOLogic.mk_UNIV ATs) (map HOLogic.mk_UNIV BTs);
@@ -265,6 +263,7 @@
       in
         Skip_Proof.prove lthy [] [] goal
           (K (stac alg_def 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
+        |> Thm.close_derivation
       end;
 
     val timer = time (timer "Algebra definition & thms");
@@ -280,8 +279,9 @@
       in
         map2 (fn goal => fn alg_set =>
           Skip_Proof.prove lthy [] []
-            goal (K (mk_alg_not_empty_tac alg_set alg_set_thms wit_thms)))
-          goals alg_set_thms
+            goal (K (mk_alg_not_empty_tac alg_set alg_set_thms wit_thms))
+          |> Thm.close_derivation)
+        goals alg_set_thms
       end;
 
     val timer = time (timer "Proved nonemptiness");
@@ -348,7 +348,7 @@
                 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 =
-          Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def));
+          Skip_Proof.prove lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
       in
         (map prove image_goals, map prove elim_goals)
       end;
@@ -361,6 +361,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
           (K (mk_mor_incl_tac mor_def map_id's))
+        |> Thm.close_derivation
       end;
 
     val mor_comp_thm =
@@ -375,6 +376,7 @@
           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ B''s @ s''s @ fs @ gs)
              (Logic.list_implies (prems, concl)))
           (K (mk_mor_comp_tac mor_def set_natural'ss map_comp_id_thms))
+        |> Thm.close_derivation
       end;
 
     val mor_inv_thm =
@@ -393,6 +395,7 @@
             (Logic.list_implies (prems, concl)))
           (K (mk_mor_inv_tac alg_def mor_def
             set_natural'ss morE_thms map_comp_id_thms map_congL_thms))
+        |> Thm.close_derivation
       end;
 
     val mor_cong_thm =
@@ -405,6 +408,7 @@
           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ fs_copy)
              (Logic.list_implies (prems, concl)))
           (K ((hyp_subst_tac THEN' atac) 1))
+        |> Thm.close_derivation
       end;
 
     val mor_str_thm =
@@ -416,6 +420,7 @@
           (fold_rev Logic.all 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
       end;
 
     val mor_convol_thm =
@@ -428,6 +433,7 @@
           (fold_rev Logic.all (s's @ prod_ss) (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
       end;
 
     val mor_UNIV_thm =
@@ -441,6 +447,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (ss @ s's @ fs) (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))))
           (K (mk_mor_UNIV_tac m morE_thms mor_def))
+        |> Thm.close_derivation
       end;
 
     val timer = time (timer "Morphism definition & thms");
@@ -471,6 +478,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs) (Logic.list_implies (prems, concl)))
           (K (mk_iso_alt_tac mor_image_thms mor_inv_thm))
+        |> Thm.close_derivation
       end;
 
     val timer = time (timer "Isomorphism definition & thms");
@@ -492,14 +500,16 @@
         val copy_str_thm = Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
             (Logic.list_implies (all_prems, alg)))
-          (K (mk_copy_str_tac set_natural'ss alg_def alg_set_thms));
+          (K (mk_copy_str_tac set_natural'ss alg_def alg_set_thms))
+          |> Thm.close_derivation;
 
         val iso = HOLogic.mk_Trueprop
           (mk_iso B's (map5 mk_s fs ss mapsBsAs yFs yFs') Bs ss inv_fs fs_copy);
         val copy_alg_thm = Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
             (Logic.list_implies (all_prems, iso)))
-          (K (mk_copy_alg_tac set_natural'ss alg_set_thms mor_def iso_alt_thm copy_str_thm));
+          (K (mk_copy_alg_tac set_natural'ss alg_set_thms mor_def iso_alt_thm copy_str_thm))
+          |> Thm.close_derivation;
 
         val ex = HOLogic.mk_Trueprop
           (list_exists_free s's
@@ -508,7 +518,8 @@
         val ex_copy_alg_thm = Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
              (Logic.list_implies (prems, ex)))
-          (K (mk_ex_copy_alg_tac n copy_str_thm copy_alg_thm));
+          (K (mk_ex_copy_alg_tac n copy_str_thm copy_alg_thm))
+          |> Thm.close_derivation;
       in
         (copy_alg_thm, ex_copy_alg_thm)
       end;
@@ -584,6 +595,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all idxs (Logic.list_implies ([prem], concl)))
           (K (mk_bd_limit_tac n suc_bd_Cinfinite))
+        |> Thm.close_derivation
       end;
 
     val timer = time (timer "Bounds");
@@ -622,7 +634,8 @@
           (Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl));
 
         val min_algs_thm = Skip_Proof.prove lthy [] [] goal
-          (K (mk_min_algs_tac suc_bd_worel in_cong'_thms));
+          (K (mk_min_algs_tac suc_bd_worel in_cong'_thms))
+          |> Thm.close_derivation;
 
         val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
 
@@ -630,9 +643,11 @@
           fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_relChain suc_bd
             (Term.absfree idx' min_alg)));
 
-        val monos = map2 (fn goal => fn min_algs =>
-          Skip_Proof.prove lthy [] [] goal (K (mk_min_algs_mono_tac min_algs)))
-            (map mk_mono_goal min_algss) min_algs_thms;
+        val monos =
+          map2 (fn goal => fn min_algs =>
+            Skip_Proof.prove lthy [] [] goal (K (mk_min_algs_mono_tac min_algs))
+            |> Thm.close_derivation)
+          (map mk_mono_goal min_algss) min_algs_thms;
 
         val Asuc_bd = mk_Asuc_bd As;
 
@@ -647,7 +662,8 @@
             (K (mk_min_algs_card_of_tac card_cT card_ct
               m suc_bd_worel min_algs_thms in_bd_sums
               sum_Card_order sum_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
-              suc_bd_Asuc_bd Asuc_bd_Cinfinite Asuc_bd_Cnotzero)));
+              suc_bd_Asuc_bd Asuc_bd_Cinfinite Asuc_bd_Cnotzero)))
+          |> Thm.close_derivation;
 
         val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
         val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_subset min_algss Bs);
@@ -659,7 +675,8 @@
             (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)));
+              suc_bd_worel min_algs_thms alg_set_thms)))
+          |> Thm.close_derivation;
       in
         (min_algs_thms, monos, card_of, least)
       end;
@@ -712,20 +729,23 @@
         val goal = fold_rev Logic.all (As @ ss) (HOLogic.mk_Trueprop (mk_alg As min_algs ss));
         val alg_min_alg = Skip_Proof.prove lthy [] [] goal
           (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sum_Cinfinite
-            set_bd_sumss min_algs_thms min_algs_mono_thms));
+            set_bd_sumss min_algs_thms min_algs_mono_thms))
+          |> Thm.close_derivation;
 
         val Asuc_bd = mk_Asuc_bd As;
         fun mk_card_of_thm min_alg def = Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (As @ ss)
             (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd)))
           (K (mk_card_of_min_alg_tac def card_of_min_algs_thm
-            suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite));
+            suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite))
+          |> Thm.close_derivation;
 
         val least_prem = HOLogic.mk_Trueprop (mk_alg As Bs ss);
         fun mk_least_thm min_alg B def = Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (As @ Bs @ ss)
             (Logic.mk_implies (least_prem, HOLogic.mk_Trueprop (mk_subset min_alg B))))
-          (K (mk_least_min_alg_tac def least_min_algs_thm));
+          (K (mk_least_min_alg_tac def least_min_algs_thm))
+          |> Thm.close_derivation;
 
         val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
 
@@ -735,11 +755,10 @@
           (fold_rev Logic.all (Bs @ ss)
             (Logic.mk_implies (incl_prem,
               HOLogic.mk_Trueprop (mk_mor incl_min_algs ss Bs ss active_ids))))
-          (K (EVERY' (rtac mor_incl_thm :: map etac leasts) 1));
+          (K (EVERY' (rtac mor_incl_thm :: map etac leasts) 1))
+          |> Thm.close_derivation;
       in
-        (alg_min_alg,
-          map2 mk_card_of_thm min_algs min_alg_defs,
-          leasts, incl)
+        (alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl)
       end;
 
     val timer = time (timer "Minimal algebra definition & thms");
@@ -821,12 +840,14 @@
     (*TODO: replace with instantiate? (problem: figure out right type instantiation)*)
     val alg_init_thm = Skip_Proof.prove lthy [] []
       (HOLogic.mk_Trueprop (mk_alg passive_UNIVs car_inits str_inits))
-      (K (rtac alg_min_alg_thm 1));
+      (K (rtac alg_min_alg_thm 1))
+      |> Thm.close_derivation;
 
     val alg_select_thm = Skip_Proof.prove lthy [] []
       (HOLogic.mk_Trueprop (mk_Ball II
         (Term.absfree iidx' (mk_alg passive_UNIVs select_Bs select_ss))))
       (mk_alg_select_tac Abs_IIT_inverse_thm)
+      |> Thm.close_derivation;
 
     val mor_select_thm =
       let
@@ -842,6 +863,7 @@
           (fold_rev Logic.all (iidx :: Bs @ ss @ Asuc_fs) (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_natural'ss str_init_defs))
+        |> Thm.close_derivation
       end;
 
     val (init_ex_mor_thm, init_unique_mor_thms) =
@@ -852,7 +874,8 @@
         val ex_mor = Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (prem, concl)))
           (mk_init_ex_mor_tac Abs_IIT_inverse_thm ex_copy_alg_thm alg_min_alg_thm
-            card_of_min_alg_thms mor_comp_thm mor_select_thm mor_incl_min_alg_thm);
+            card_of_min_alg_thms mor_comp_thm mor_select_thm mor_incl_min_alg_thm)
+          |> Thm.close_derivation;
 
         val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits
         val mor_prems = map HOLogic.mk_Trueprop
@@ -865,7 +888,8 @@
           (fold_rev Logic.all (init_xs @ Bs @ ss @ init_fs @ init_fs_copy)
             (Logic.list_implies (prems @ mor_prems, unique)))
           (K (mk_init_unique_mor_tac m alg_def alg_init_thm least_min_alg_thms
-            in_mono'_thms alg_set_thms morE_thms map_congs));
+            in_mono'_thms alg_set_thms morE_thms map_congs))
+          |> Thm.close_derivation;
       in
         (ex_mor, split_conj_thm unique_mor)
       end;
@@ -898,6 +922,7 @@
         Skip_Proof.prove lthy [] []
           (fold_rev Logic.all init_phis (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
       end;
 
     val timer = time (timer "Initiality definition & thms");
@@ -929,7 +954,8 @@
     fun mk_inver_thm mk_tac rep abs X thm =
       Skip_Proof.prove lthy [] []
         (HOLogic.mk_Trueprop (mk_inver rep abs X))
-        (K (EVERY' [rtac ssubst, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1));
+        (K (EVERY' [rtac ssubst, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1))
+      |> Thm.close_derivation;
 
     val inver_Reps = map4 (mk_inver_thm rtac) Abs_Ts Rep_Ts (map HOLogic.mk_UNIV Ts) Rep_inverses;
     val inver_Abss = map4 (mk_inver_thm etac) Rep_Ts Abs_Ts car_inits
@@ -1009,13 +1035,15 @@
         val mor_Rep =
           Skip_Proof.prove lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs flds car_inits str_inits Rep_Ts))
-            (mk_mor_Rep_tac fld_defs copy bijs inver_Abss inver_Reps);
+            (mk_mor_Rep_tac fld_defs copy bijs inver_Abss inver_Reps)
+          |> Thm.close_derivation;
 
         val inv = mor_inv_thm OF [mor_Rep, talg_thm, alg_init_thm];
         val mor_Abs =
           Skip_Proof.prove lthy [] []
             (HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs flds Abs_Ts))
-            (K (mk_mor_Abs_tac inv inver_Abss inver_Reps));
+            (K (mk_mor_Abs_tac inv inver_Abss inver_Reps))
+          |> Thm.close_derivation;
       in
         (mor_Rep, mor_Abs)
       end;
@@ -1068,6 +1096,7 @@
           (Skip_Proof.prove lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs flds active_UNIVs ss (map (mk_iter Ts ss) ks)))
             (K (mk_mor_iter_tac cT ct iter_defs ex_mor (mor_comp RS mor_cong))))
+        |> Thm.close_derivation
       end;
 
     val iter_thms = map (fn morE => rule_by_tactic lthy
@@ -1082,7 +1111,8 @@
         val unique_mor = Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (ss @ fs) (Logic.mk_implies (prem, unique)))
           (K (mk_iter_unique_mor_tac type_defs init_unique_mor_thms T_subset2s Reps
-            mor_comp_thm mor_Abs_thm mor_iter_thm));
+            mor_comp_thm mor_Abs_thm mor_iter_thm))
+          |> Thm.close_derivation;
       in
         `split_conj_thm unique_mor
       end;
@@ -1149,8 +1179,9 @@
       in
         map5 (fn goal => fn unf_def => fn iter => fn map_comp_id => fn map_congL =>
           Skip_Proof.prove lthy [] [] goal
-            (K (mk_unf_o_fld_tac unf_def iter map_comp_id map_congL fld_o_iter_thms)))
-          goals unf_defs iter_thms map_comp_id_thms map_congL_thms
+            (K (mk_unf_o_fld_tac unf_def iter map_comp_id map_congL fld_o_iter_thms))
+          |> Thm.close_derivation)
+        goals unf_defs iter_thms map_comp_id_thms map_congL_thms
       end;
 
     val unf_fld_thms = map (fn thm => thm RS @{thm pointfree_idE}) unf_o_fld_thms;
@@ -1228,7 +1259,8 @@
         val goals = map5 mk_goal ks rec_ss rec_maps_rev flds xFs;
       in
         map2 (fn goal => fn iter =>
-          Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iter fst_rec_pair_thms))
+          Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iter fst_rec_pair_thms)
+          |> Thm.close_derivation)
         goals iter_thms
       end;
 
@@ -1263,7 +1295,9 @@
         (Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (phis @ Izs) goal)
           (K (mk_fld_induct_tac m set_natural'ss init_induct_thm morE_thms mor_Abs_thm
-            Rep_inverses Abs_inverses Reps T_subset1s T_subset2s)), rev (Term.add_tfrees goal []))
+            Rep_inverses Abs_inverses Reps T_subset1s T_subset2s))
+        |> Thm.close_derivation,
+        rev (Term.add_tfrees goal []))
       end;
 
     val cTs = map (SOME o certifyT lthy o TFree) induct_params;
@@ -1303,7 +1337,8 @@
       in
         (singleton (Proof_Context.export names_lthy lthy)
           (Skip_Proof.prove lthy [] [] goal
-            (mk_fld_induct2_tac cTs cts fld_induct_thm weak_fld_induct_thms)),
+            (mk_fld_induct2_tac cTs cts fld_induct_thm weak_fld_induct_thms))
+          |> Thm.close_derivation,
         rev (Term.add_tfrees goal []))
       end;
 
@@ -1367,9 +1402,10 @@
               (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_comp (fs_map, fld),
                 HOLogic.mk_comp (fld', Term.list_comb (map, fs @ fs_maps)))));
             val goals = map4 mk_goal fs_maps map_FTFT's flds fld's;
-            val maps = map4 (fn goal => fn iter => fn map_comp_id => fn map_cong =>
-              Skip_Proof.prove lthy [] [] goal
-                (K (mk_map_tac m n iter map_comp_id map_cong)))
+            val maps =
+              map4 (fn goal => fn iter => fn map_comp_id => fn map_cong =>
+                Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iter map_comp_id map_cong))
+                |> Thm.close_derivation)
               goals iter_thms map_comp_id_thms map_congs;
           in
             map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
@@ -1386,7 +1422,8 @@
                 (map2 (curry HOLogic.mk_eq) us fs_maps));
             val unique = Skip_Proof.prove lthy [] []
               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
-              (K (mk_map_unique_tac m mor_def iter_unique_mor_thm map_comp_id_thms map_congs));
+              (K (mk_map_unique_tac m mor_def iter_unique_mor_thm map_comp_id_thms map_congs))
+              |> Thm.close_derivation;
           in
             `split_conj_thm unique
           end;
@@ -1427,7 +1464,7 @@
             val goalss =
               map3 (fn sets => map4 (mk_goal sets) flds sets) setss_by_range colss map_setss;
             val setss = map (map2 (fn iter => fn goal =>
-              Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iter)))
+              Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iter)) |> Thm.close_derivation)
               iter_thms) goalss;
 
             fun mk_simp_goal pas_set act_sets sets fld z set =
@@ -1442,8 +1479,9 @@
 
             val set_simpss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
                 Skip_Proof.prove lthy [] [] goal
-                  (K (mk_set_simp_tac set (nth set_nats (i - 1)) (drop m set_nats))))
-                set_natural'ss) ls simp_goalss setss;
+                  (K (mk_set_simp_tac set (nth set_nats (i - 1)) (drop m set_nats)))
+                |> Thm.close_derivation)
+              set_natural'ss) ls simp_goalss setss;
           in
             (set_simpss, setss)
           end;
@@ -1485,10 +1523,11 @@
                   fs setss_by_range setss_by_range';
 
             fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_natural'ss map_simp_thms;
-            val thms = map5 (fn goal => fn csets => fn set_simps => fn induct => fn i =>
-              singleton (Proof_Context.export names_lthy lthy)
-                (Skip_Proof.prove lthy [] [] goal
-                  (mk_tac induct csets set_simps i)))
+            val thms =
+              map5 (fn goal => fn csets => fn set_simps => fn induct => fn i =>
+                singleton (Proof_Context.export names_lthy lthy)
+                  (Skip_Proof.prove lthy [] [] goal (mk_tac induct csets set_simps i))
+                |> Thm.close_derivation)
               goals csetss set_simp_thmss inducts ls;
           in
             map split_conj_thm thms
@@ -1511,9 +1550,11 @@
                   (map2 mk_set_bd Izs sets))) setss_by_range;
 
             fun mk_tac induct = mk_set_bd_tac m (rtac induct) bd_Cinfinite set_bd_cpowss;
-            val thms = map4 (fn goal => fn set_simps => fn induct => fn i =>
-              singleton (Proof_Context.export names_lthy lthy)
-                (Skip_Proof.prove lthy [] [] goal (mk_tac induct set_simps i)))
+            val thms =
+              map4 (fn goal => fn set_simps => fn induct => fn i =>
+                singleton (Proof_Context.export names_lthy lthy)
+                  (Skip_Proof.prove lthy [] [] goal (mk_tac induct set_simps i))
+                |> Thm.close_derivation)
               goals set_simp_thmss inducts ls;
           in
             map split_conj_thm thms
@@ -1542,7 +1583,8 @@
 
             val thm = singleton (Proof_Context.export names_lthy lthy)
               (Skip_Proof.prove lthy [] [] goal
-              (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs map_simp_thms));
+              (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs map_simp_thms))
+              |> Thm.close_derivation;
           in
             split_conj_thm thm
           end;
@@ -1568,7 +1610,8 @@
 
             val thm = singleton (Proof_Context.export names_lthy lthy)
               (Skip_Proof.prove lthy [] [] goal
-              (mk_incl_min_alg_tac (rtac induct) Fset_set_thmsss alg_set_thms alg_min_alg_thm));
+              (mk_incl_min_alg_tac (rtac induct) Fset_set_thmsss alg_set_thms alg_min_alg_thm))
+              |> Thm.close_derivation;
           in
             split_conj_thm thm
           end;
@@ -1610,7 +1653,8 @@
             val thm = singleton (Proof_Context.export names_lthy lthy)
               (Skip_Proof.prove lthy [] [] goal
               (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls map_simp_thms
-                (transpose set_simp_thmss) Fset_set_thmsss fld_inject_thms)));
+                (transpose set_simp_thmss) Fset_set_thmsss fld_inject_thms)))
+              |> Thm.close_derivation;
           in
             split_conj_thm thm
           end;
@@ -1708,7 +1752,8 @@
               fn set_naturals => fn set_incls => fn set_set_inclss =>
               Skip_Proof.prove lthy [] [] goal
                (K (mk_rel_unfold_tac in_Irels i in_rel map_comp map_cong map_simp set_simps
-                 fld_inject fld_unf set_naturals set_incls set_set_inclss)))
+                 fld_inject fld_unf set_naturals set_incls set_set_inclss))
+              |> Thm.close_derivation)
             ks goals in_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
               fld_inject_thms fld_unf_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
           end;
@@ -1721,37 +1766,58 @@
             val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis;
           in
             map3 (fn goal => fn pred_def => fn Irel_unfold =>
-              Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Ipred_defs Irel_unfold))
+              Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Ipred_defs Irel_unfold)
+              |> Thm.close_derivation)
             goals pred_defs Irel_unfold_thms
           end;
 
         val timer = time (timer "additional properties");
 
         val ls' = if m = 1 then [0] else ls
+
+        val Ibnf_common_notes =
+          [(map_uniqueN, [fold_maps map_unique_thm])]
+          |> map (fn (thmN, thms) =>
+            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
+
+        val Ibnf_notes =
+          [(map_simpsN, map single folded_map_simp_thms),
+          (set_inclN, set_incl_thmss),
+          (set_set_inclN, map flat set_set_incl_thmsss), (* nicer names? *)
+          (rel_unfoldN, map single Irel_unfold_thms),
+          (pred_unfoldN, map single Ipred_unfold_thms)] @
+          map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
+          |> maps (fn (thmN, thmss) =>
+            map2 (fn b => fn thms =>
+              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
+            bs thmss)
       in
-        lthy
-        |> note map_uniqueN [fold_maps map_unique_thm]
-        |> notes map_simpsN (map single folded_map_simp_thms)
-        |> fold2 (fn i => notes (mk_set_simpsN i) o map single) ls' folded_set_simp_thmss
-        |> notes set_inclN set_incl_thmss
-        |> notes set_set_inclN (map flat set_set_incl_thmsss)
-        |> notes rel_unfoldN (map single Irel_unfold_thms)
-        |> notes pred_unfoldN (map single Ipred_unfold_thms)
+        lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd
       end;
 
+      val common_notes =
+        [(fld_inductN, [fld_induct_thm]),
+        (fld_induct2N, [fld_induct2_thm])]
+        |> map (fn (thmN, thms) =>
+          ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
+
+      val notes =
+        [(iterN, iter_thms),
+        (iter_uniqueN, iter_unique_thms),
+        (recN, rec_thms),
+        (unf_fldN, unf_fld_thms),
+        (fld_unfN, fld_unf_thms),
+        (unf_injectN, unf_inject_thms),
+        (unf_exhaustN, unf_exhaust_thms),
+        (fld_injectN, fld_inject_thms),
+        (fld_exhaustN, fld_exhaust_thms)]
+        |> map (apsnd (map single))
+        |> maps (fn (thmN, thmss) =>
+          map2 (fn b => fn thms =>
+            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
+          bs thmss)
   in
-    lthy
-    |> notes iterN (map single iter_thms)
-    |> notes iter_uniqueN (map single iter_unique_thms)
-    |> notes recN (map single rec_thms)
-    |> notes unf_fldN (map single unf_fld_thms)
-    |> notes fld_unfN (map single fld_unf_thms)
-    |> notes unf_injectN (map single unf_inject_thms)
-    |> notes unf_exhaustN (map single unf_exhaust_thms)
-    |> notes fld_injectN (map single fld_inject_thms)
-    |> notes fld_exhaustN (map single fld_exhaust_thms)
-    |> note fld_inductN [fld_induct_thm]
-    |> note fld_induct2N [fld_induct2_thm]
+    lthy |> Local_Theory.notes (common_notes @ notes) |> snd
   end;
 
 val _ =