src/HOL/Tools/BNF/bnf_gfp.ML

         val goal = mk_Trueprop_eq (lhs, rhs);
         val vars = Variable.add_free_names lthy goal [];
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
 
     (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>

         val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
         val vars = Variable.add_free_names lthy goal [];
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
           (fn {context = ctxt, prems = _} => mk_map_cong0L_tac ctxt m map_cong0 map_id)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
     val in_mono'_thms = map (fn thm =>
       (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;

       in
         map (fn goal =>
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             (hyp_subst_tac ctxt THEN' rtac ctxt refl) 1))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals
       end;
 
     val timer = time (timer "Derived simple theorems");
 

       in
         map (fn goals => map (fn goal =>
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             mk_coalg_set_tac ctxt coalg_def))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals) goalss
       end;
 
     fun mk_tcoalg BTs = mk_coalg (map HOLogic.mk_UNIV BTs);
 

       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => (rtac ctxt (coalg_def RS iffD2) 1 THEN CONJ_WRAP
             (K (EVERY' [rtac ctxt ballI, rtac ctxt CollectI,
               CONJ_WRAP' (K (EVERY' [rtac ctxt @{thm subset_UNIV}])) allAs] 1)) ss))
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val timer = time (timer "Coalgebra definition & thms");
 
     (* morphism *)

         val elim_goals = @{map 6} mk_elim_goal Bs mapsAsBs fs ss s's zs;
         fun prove goal =
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             mk_mor_elim_tac ctxt mor_def))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         (map prove image_goals, map prove elim_goals)
       end;
 
     val mor_image'_thms = map (fn thm => @{thm set_mp} OF [thm, imageI]) mor_image_thms;

         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
         val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => mk_mor_incl_tac ctxt mor_def map_ids)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);
 
     val mor_comp_thm =

         val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} =>
             mk_mor_comp_tac ctxt mor_def mor_image'_thms morE_thms map_comp_id_thms)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_cong_thm =
       let
         val prems = map HOLogic.mk_Trueprop

         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs_copy);
         val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_UNIV_thm =
       let
         fun mk_conjunct mapAsBs f s s' = HOLogic.mk_eq

         val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's);
         val vars = fold (Variable.add_free_names lthy) [lhs, rhs] [];
       in
         Goal.prove_sorry lthy vars [] (mk_Trueprop_eq (lhs, rhs))
           (fn {context = ctxt, prems = _} => mk_mor_UNIV_tac ctxt morE_thms mor_def)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_str_thm =
       let
         val maps = map2 (fn Ds => fn bnf => Term.list_comb

         val goal = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss);
         val vars = Variable.add_free_names lthy goal [];
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_UNIV_thm)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val timer = time (timer "Morphism definition & thms");
 
     (* bisimulation *)

         val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs_copy);
         val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' assume_tac ctxt) 1)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val bis_rel_thm =
       let
         fun mk_conjunct R s s' b1 b2 rel =

         val vars = Variable.add_free_names lthy goal [];
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_bis_rel_tac ctxt m bis_def in_rels map_comps
             map_cong0s set_mapss)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val bis_converse_thm =
       let
         val goal = Logic.mk_implies (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),

         val vars = Variable.add_free_names lthy goal [];
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_bis_converse_tac ctxt m bis_rel_thm rel_congs
             rel_converseps)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val bis_O_thm =
       let
         val prems =

           HOLogic.mk_Trueprop (mk_bis Bs ss B''s s''s (map2 (curry mk_rel_comp) Rs R's));
         val vars = fold (Variable.add_free_names lthy) (concl :: prems) [];
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => mk_bis_O_tac ctxt m bis_rel_thm rel_congs le_rel_OOs)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val bis_Gr_thm =
       let
         val concl = HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map2 mk_Gr Bs fs));
         val vars = fold (Variable.add_free_names lthy) ([coalg_prem, mor_prem, concl]) [];
       in
         Goal.prove_sorry lthy vars [] (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
+        |> Thm.close_derivation \<^here>
       end;
 
     val bis_image2_thm = bis_cong_thm OF
       ((bis_O_thm OF [bis_Gr_thm RS bis_converse_thm, bis_Gr_thm]) ::
       replicate n @{thm image2_Gr});

           HOLogic.mk_Trueprop (mk_bis Bs ss B's s's (map (mk_UNION Idx) Ris));
         val vars = fold (Variable.add_free_names lthy) [prem, concl] [];
       in
         Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl))
           (fn {context = ctxt, prems = _} => mk_bis_Union_tac ctxt bis_def in_mono'_thms)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     (* self-bisimulation *)
 
     fun mk_sbis Bs ss Rs = mk_bis Bs ss Bs ss Rs;

         val vars = Variable.add_free_names lthy goal [];
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} =>
             mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union_thm bis_cong_thm)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val lsbis_incl_thms = map (fn i => sbis_lsbis_thm RS
       (bis_def RS iffD1 RS conjunct1 RS mk_conjunctN n i)) ks;
     val lsbisE_thms = map (fn i => (mk_specN 2 (sbis_lsbis_thm RS

       in
         @{map 3} (fn goal => fn i => fn def =>
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             mk_incl_lsbis_tac ctxt n i def))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals ks lsbis_defs
       end;
 
     val equiv_lsbis_thms =
       let

         @{map 3} (fn goal => fn l_incl => fn incl_l =>
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal
             (fn {context = ctxt, prems = _} => mk_equiv_lsbis_tac ctxt sbis_lsbis_thm l_incl incl_l
               bis_Id_on_thm bis_converse_thm bis_O_thm)
-          |> Thm.close_derivation))
+          |> Thm.close_derivation \<^here>))
         goals lsbis_incl_thms incl_lsbis_thms
       end;
 
     val timer = time (timer "Bisimulations");
 

 
     val coalgT_thm =
       Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop (mk_coalg carTAs strTAs))
         (fn {context = ctxt, prems = _} => mk_coalgT_tac ctxt m
           (coalg_def :: isNode_defs @ carT_defs) strT_defs set_mapss)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     val timer = time (timer "Tree coalgebra");
 
     fun mk_to_sbd s x i i' =
       mk_toCard (nth (nth setssAs (i - 1)) (m + i' - 1) $ (s $ x)) sbd;

         val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree nat' goal, nat];
 
         val length_Lev =
           Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
             (fn {context = ctxt, prems = _} => mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         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 = Logic.mk_implies

         val length_Levs' =
           map2 (fn goal => fn length_Lev =>
             Variable.add_free_names lthy goal []
             |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
               mk_length_Lev'_tac ctxt length_Lev))
-            |> Thm.close_derivation)
+            |> Thm.close_derivation \<^here>)
           goals length_Levs;
       in
         (length_Levs, length_Levs')
       end;
 

         val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree kl' goal, kl];
 
         val rv_last =
           Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
             (fn {context = ctxt, prems = _} => mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val rv_last' = mk_specN (n + 1) rv_last;
       in
         map (fn i => map (fn i' => rv_last' RS mk_conjunctN n i RS mk_conjunctN n i') ks) ks
       end;

 
         val set_Lev =
           Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
             (fn {context = ctxt, prems = _} =>
               mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbd_thmss)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val set_Lev' = mk_specN (3 * n + 1) set_Lev;
       in
         map (fn i => map (fn i' => map (fn i'' => set_Lev' RS
           mk_conjunctN n i RS mp RS

         val set_image_Lev =
           Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
             (fn {context = ctxt, prems = _} =>
               mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss
                 from_to_sbd_thmss to_sbd_inj_thmss)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val set_image_Lev' = mk_specN (2 * n + 2) set_image_Lev;
       in
         map (fn i => map (fn i' => map (fn i'' => set_image_Lev' RS
           mk_conjunctN n i RS mp RS

           (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 \<^here>
       end;
 
     val timer = time (timer "Behavioral morphism");
 
     val lsbisAs = map (mk_lsbis carTAs strTAs) ks;

       in
         @{map 4} (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
           Goal.prove_sorry lthy [] [] goal
             (fn {context = ctxt, prems = _} => mk_congruent_str_final_tac ctxt m lsbisE map_comp_id
               map_cong0 equiv_LSBIS_thms)
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals lsbisE_thms map_comp_id_thms map_cong0s
       end;
 
     val coalg_final_thm = Goal.prove_sorry lthy [] []
       (HOLogic.mk_Trueprop (mk_coalg car_finals str_finals))
       (fn {context = ctxt, prems = _} => mk_coalg_final_tac ctxt m coalg_def
         congruent_str_final_thms equiv_LSBIS_thms set_mapss coalgT_set_thmss)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     val mor_T_final_thm = Goal.prove_sorry lthy [] []
       (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finals str_finals (map mk_proj lsbisAs)))
       (fn {context = ctxt, prems = _} => mk_mor_T_final_tac ctxt mor_def congruent_str_final_thms
         equiv_LSBIS_thms)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     val mor_final_thm = mor_comp_thm OF [mor_beh_thm, mor_T_final_thm];
     val in_car_final_thms = map (fn thm => thm OF [mor_final_thm, UNIV_I]) mor_image'_thms;
 
     val timer = time (timer "Final coalgebra");

         val mor_Rep =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
             (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt (mor_def :: dtor_defs) Reps
               Abs_inverses coalg_final_set_thmss map_comp_id_thms map_cong0L_thms)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val mor_Abs =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor car_finals str_finals UNIVs dtors Abs_Ts))
             (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt (mor_def :: dtor_defs)
               Abs_inverses)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         (mor_Rep, mor_Abs)
       end;
 
     val timer = time (timer "dtor definitions & thms");

         val vars = Variable.add_free_names lthy goal [];
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_mor_unfold_tac ctxt m mor_UNIV_thm dtor_defs
             unfold_defs Abs_inverses' morEs' map_comp_id_thms map_cong0s)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
     val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
 
     val (raw_coind_thms, raw_coind_thm) =
       let

       in
         `split_conj_thm (Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl))
           (fn {context = ctxt, prems = _} => mk_raw_coind_tac ctxt 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 \<^here>)
       end;
 
     val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
       let
         val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors unfold_fs);

         val mor_thm = mor_comp_thm OF [mor_final_thm, mor_Abs_thm];
 
         val unique_mor = Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
           (fn {context = ctxt, prems = _} => mk_unfold_unique_mor_tac ctxt raw_coind_thms
             bis_thm mor_thm unfold_defs)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         `split_conj_thm unique_mor
       end;
 
     val (dtor_unfold_unique_thms, dtor_unfold_unique_thm) = `split_conj_thm (split_conj_prems n

       in
         @{map 5} (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
           Goal.prove_sorry lthy [] [] goal
             (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id
               map_cong0L unfold_o_dtor_thms)
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
           goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms
       end;
 
     val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
     val ctor_dtor_thms = map (fn thm => thm RS @{thm pointfree_idE}) ctor_o_dtor_thms;

         val dtor_coinduct =
           Variable.add_free_names lthy dtor_coinduct_goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] dtor_coinduct_goal
             (fn {context = ctxt, prems = _} => mk_dtor_coinduct_tac ctxt m raw_coind_thm bis_rel_thm
               rel_congs))
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         (rev (Term.add_tfrees dtor_coinduct_goal []), dtor_coinduct)
       end;
 
     val timer = time (timer "coinduction");

               @{map 5} (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong =>
                 Variable.add_free_names lthy goal []
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
                      mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               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
           end;
 

             val vars = fold (Variable.add_free_names lthy) (goal :: prems) [];
           in
             `split_conj_thm (Goal.prove_sorry lthy vars [] (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)
+            |> Thm.close_derivation \<^here>)
           end;
 
         val Jmap_comp0_thms =
           let
             val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj

             val vars = Variable.add_free_names lthy goal [];
           in
             split_conj_thm (Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} =>
                 mk_map_comp0_tac ctxt Jmap_thms map_comp0s dtor_Jmap_unique_thm)
-              |> Thm.close_derivation)
+              |> Thm.close_derivation \<^here>)
           end;
 
         val timer = time (timer "map functions for the new codatatypes");
 
         val Jset_minimal_thms =

                 @{map 4} (fn goal => fn cts => fn col_0s => fn col_Sucs =>
                   Variable.add_free_names lthy goal []
                   |> (fn vars => Goal.prove_sorry lthy vars [] goal
                     (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
                       col_Sucs))
-                  |> Thm.close_derivation)
+                  |> Thm.close_derivation \<^here>)
                 goals ctss col_0ss' col_Sucss'
               end;
 
             fun mk_conjunct set K x = mk_leq (set $ x) (K $ x);
             fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (@{map 3} mk_conjunct sets Ks Jzs);

             map2 (fn goal => fn col_minimal =>
                 Variable.add_free_names lthy goal []
                 |> (fn vars => Goal.prove_sorry lthy vars [] 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 \<^here>)
             goals col_minimal_thms
           end;
 
         val (dtor_Jset_incl_thmss, dtor_set_Jset_incl_thmsss) =
           let

               map2 (fn goal => fn rec_Suc =>
                 Variable.add_free_names lthy goal []
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
                     mk_set_incl_Jset_tac ctxt rec_Suc))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               goals rec_Sucs)
             set_incl_Jset_goalss col_Sucss,
             map2 (fn goalss => fn rec_Sucs =>
               map2 (fn k => fn goals =>
                 map2 (fn goal => fn rec_Suc =>
                   Variable.add_free_names lthy goal []
                   |> (fn vars => Goal.prove_sorry lthy vars [] goal
                     (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
                       mk_set_Jset_incl_Jset_tac ctxt n rec_Suc k))
-                  |> Thm.close_derivation)
+                  |> Thm.close_derivation \<^here>)
                 goals rec_Sucs)
               ks goalss)
             set_Jset_incl_Jset_goalsss col_Sucss)
           end;
 

               (@{map 4} (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss =>
                 Variable.add_free_names lthy goal []
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} =>
                     mk_set_le_tac ctxt n Jset_minimal set_Jsets set_Jset_Jsetss))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss');
 
             val ge_goalss = map (map HOLogic.mk_Trueprop) (mk_goals (uncurry mk_leq o swap));
             val set_ge_thmss =
               @{map 3} (@{map 3} (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
                 Variable.add_free_names lthy goal []
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} =>
                     mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets))
-                |> Thm.close_derivation))
+                |> Thm.close_derivation \<^here>))
               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
             |> `transpose
           end;

               @{map 4} (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
                 Variable.add_free_names lthy goal []
                 |> (fn vars => Goal.prove_sorry lthy vars [] (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)
+                |> Thm.close_derivation \<^here>)
               goals ctss col_0ss' col_Sucss';
           in
             map (split_conj_thm o mk_specN n) thms
           end;
 

               @{map 5} (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
                 Variable.add_free_names lthy goal []
                 |> (fn vars => Goal.prove_sorry lthy vars [] (HOLogic.mk_Trueprop goal)
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN
                     mk_col_bd_tac ctxt m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               ls goals ctss col_0ss' col_Sucss';
           in
             map (split_conj_thm o mk_specN n) thms
           end;
 

             val thm =
               Goal.prove_sorry lthy vars [] goal
                 (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt m (rtac ctxt coinduct) map_comps
                   dtor_Jmap_thms map_cong0s
                   set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels)
-              |> Thm.close_derivation;
+              |> Thm.close_derivation \<^here>;
           in
             split_conj_thm thm
           end;
 
         val in_Jrels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD})

               Variable.add_free_names lthy goal []
               |> (fn vars => Goal.prove_sorry lthy vars [] goal
                 (fn {context = ctxt, prems = _} =>
                   mk_dtor_rel_tac ctxt 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 \<^here>)
             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
           end;
 

               Goal.prove_sorry lthy vars [] (Logic.list_implies (helper_prems, concl))
                 (fn {context = ctxt, prems = _} =>
                   mk_rel_coinduct_coind_tac ctxt fst m
                     (infer_instantiate' ctxt cts dtor_coinduct_thm) ks map_comps map_cong0s
                     map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms in_rels)
-              |> Thm.close_derivation
+              |> Thm.close_derivation \<^here>
               |> split_conj_thm
             end;
 
           val helper_coind1_thms = mk_helper_coind_thms true helper_coind1_concl cts1;
           val helper_coind2_thms = mk_helper_coind_thms false helper_coind2_concl cts2;

               fold (Variable.add_free_names lthy) (concl :: helper_prems) []
               |> (fn vars => Goal.prove_sorry lthy vars [] (Logic.list_implies (helper_prems, concl))
                 (fn {context = ctxt, prems = _} =>
                   mk_rel_coinduct_ind_tac ctxt m ks
                     dtor_unfold_thms set_mapss j (infer_instantiate' ctxt cts set_induct)))
-              |> Thm.close_derivation
+              |> Thm.close_derivation \<^here>
               |> split_conj_thm)
             mk_helper_ind_concls ls dtor_Jset_induct_thms ctss
             |> transpose;
         in
           mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels

             val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
             val vars = Variable.add_free_names lthy goal [];
           in
             Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
               mk_le_rel_OO_tac ctxt Jrel_coinduct_thm dtor_Jrel_thms le_rel_OOs)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val timer = time (timer "helpers for BNF properties");
 
         fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit);

             map2 (fn goal => fn induct =>
               Variable.add_free_names lthy goal []
               |> (fn vars => Goal.prove_sorry lthy vars [] 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 \<^here>)
             goals dtor_Jset_induct_thms
             |> map split_conj_thm
             |> transpose
             |> map (map_filter (try (fn thm => thm RS bspec RS mp)))
             |> curry op ~~ (map_index Library.I (map (close_wit I) wits))