src/HOL/Tools/BNF/bnf_lfp.ML

           take m all_gs @ map HOLogic.mk_comp (drop m all_gs ~~ fs)) $ x;
         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_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 = fold (Variable.add_free_names lthy) (goal :: prems) [];
       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 bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
     val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;

       in
         map (fn goal =>
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
             mk_alg_set_tac ctxt alg_def))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals
       end;
 
     val timer = time (timer "Algebra definition & thms");
 

         map2 (fn goal => fn alg_set =>
           Variable.add_free_names lthy goal []
           |> (fn vars => Goal.prove_sorry lthy vars [] goal
             (fn {context = ctxt, prems = _} =>
               mk_alg_not_empty_tac ctxt alg_set alg_set_thms wit_thms))
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals alg_set_thms
       end;
 
     val timer = time (timer "Proved nonemptiness");
 

         val elim_goals = @{map 7} mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
         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 elim_goals
       end;
 
     val mor_incl_thm =

         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_comp_thm =
       let
         val prems =

           HOLogic.mk_Trueprop (mk_mor Bs ss B''s s''s (map2 (curry HOLogic.mk_comp) gs fs));
         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 set_mapss 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_str_thm =
       let
         val maps = map2 (fn Ds => fn bnf => Term.list_comb

           (mk_mor (map HOLogic.mk_UNIV FTsAs) maps active_UNIVs ss 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_def)
-        |> 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 m morE_thms mor_def)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val timer = time (timer "Morphism definition & thms");
 
     (* bounds *)

           (Term.absfree jdx' (Library.foldr1 HOLogic.mk_conj (map mk_conjunct idxs))));
         val vars = fold (Variable.add_free_names lthy) [prem, concl] [];
       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies ([prem], concl))
           (fn {context = ctxt, prems = _} => mk_bd_limit_tac ctxt n suc_bd_Cinfinite)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val timer = time (timer "Bounds");
 
     (* minimal algebra *)

         val goal = Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl);
         val vars = Variable.add_free_names lthy goal [];
 
         val min_algs_thm = Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_min_algs_tac ctxt suc_bd_worel in_cong'_thms)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         val min_algs_thms = map (fn k => min_algs_thm RS mk_nthI n k) ks;
 
         fun mk_mono_goal min_alg =
           HOLogic.mk_Trueprop (mk_relChain suc_bd (Term.absfree idx' min_alg));

         val monos =
           map2 (fn goal => fn min_algs =>
             Variable.add_free_names lthy goal []
             |> (fn vars => Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_min_algs_mono_tac ctxt min_algs))
-            |> Thm.close_derivation)
+            |> Thm.close_derivation \<^here>)
           (map mk_mono_goal min_algss) min_algs_thms;
 
         fun mk_card_conjunct min_alg = mk_ordLeq (mk_card_of min_alg) Asuc_bd;
         val card_conjunction = Library.foldr1 HOLogic.mk_conj (map mk_card_conjunct min_algss);
         val card_cT = Thm.ctyp_of lthy suc_bdT;

             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_min_algs_card_of_tac ctxt card_cT card_ct
                 m suc_bd_worel min_algs_thms in_sbds
                 sbd_Card_order sbd_Cnotzero suc_bd_Card_order suc_bd_Cinfinite suc_bd_Cnotzero
                 suc_bd_Asuc_bd Asuc_bd_Cinfinite)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val least_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val least_conjunction = Library.foldr1 HOLogic.mk_conj (map2 mk_leq min_algss Bs);
         val least_cT = Thm.ctyp_of lthy suc_bdT;

             val vars = Variable.add_free_names lthy goal [];
           in
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_min_algs_least_tac ctxt least_cT least_ct
                 suc_bd_worel min_algs_thms alg_set_thms)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
       in
         (min_algs_thms, monos, card_of, least)
       end;
 

             val vars = Variable.add_free_names lthy goal [];
           in
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_alg_min_alg_tac ctxt m alg_def min_alg_defs
                 suc_bd_limit_thm sbd_Cinfinite set_sbdss min_algs_thms min_algs_mono_thms)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         fun mk_card_of_thm min_alg def =
           let
             val goal = HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd);
             val vars = Variable.add_free_names lthy goal [];
           in
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_card_of_min_alg_tac ctxt def card_of_min_algs_thm
                 suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         fun mk_least_thm min_alg B def =
           let
             val prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
             val goal = Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq min_alg B));
             val vars = Variable.add_free_names lthy goal [];
           in
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} => mk_least_min_alg_tac ctxt def least_min_algs_thm)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val leasts = @{map 3} mk_least_thm min_algs Bs min_alg_defs;
 
         val incl =

             val vars = Variable.add_free_names lthy goal [];
           in
             Goal.prove_sorry lthy vars [] goal
               (fn {context = ctxt, prems = _} =>
                 EVERY' (rtac ctxt mor_incl_thm :: map (etac ctxt) leasts) 1)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
       in
         (alg_min_alg, map2 mk_card_of_thm min_algs min_alg_defs, leasts, incl)
       end;
 

 
     val alg_select_thm = Goal.prove_sorry lthy [] []
       (HOLogic.mk_Trueprop (mk_Ball II
         (Term.absfree iidx' (mk_alg select_Bs select_ss))))
       (fn {context = ctxt, prems = _} => mk_alg_select_tac ctxt Abs_IIT_inverse_thm)
-      |> Thm.close_derivation;
+      |> Thm.close_derivation \<^here>;
 
     val mor_select_thm =
       let
         val i_prem = mk_Trueprop_mem (iidx, II);
         val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss active_UNIVs ss Asuc_fs);

       in
         Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, concl))
           (fn {context = ctxt, prems = _} => mk_mor_select_tac ctxt mor_def mor_cong_thm
             mor_comp_thm mor_incl_min_alg_thm alg_def alg_select_thm alg_set_thms set_mapss
             str_init_defs)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val init_unique_mor_thms =
       let
         val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits

         val vars = fold (Variable.add_free_names lthy) (unique :: all_prems) [];
         val unique_mor =
           Goal.prove_sorry lthy vars [] (Logic.list_implies (all_prems, unique))
             (fn {context = ctxt, prems = _} => mk_init_unique_mor_tac ctxt cts m alg_def
               alg_init_thm least_min_alg_thms in_mono'_thms alg_set_thms morE_thms map_cong0s)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         split_conj_thm unique_mor
       end;
 
     val init_setss = mk_setss (passiveAs @ active_initTs);

         val vars = fold (Variable.add_free_names lthy) [concl, prem] [];
       in
         Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, concl))
           (fn {context = ctxt, prems = _} => mk_init_induct_tac ctxt m alg_def alg_init_thm
             least_min_alg_thms alg_set_thms)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val timer = time (timer "Initiality definition & thms");
 
     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =

         val mor_Rep =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
             (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m defs Reps Abs_inverses
               alg_min_alg_thm alg_set_thms set_mapss)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
 
         fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
         val cts = @{map 3} (Thm.cterm_of lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
 
         val mor_Abs =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs ctors Abs_Ts))
             (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt cts defs Abs_inverses
               map_comp_id_thms map_cong0L_thms)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         (mor_Rep, mor_Abs)
       end;
 
     val timer = time (timer "ctor definitions & thms");

         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_copy_tac ctxt m alg_def mor_def alg_set_thms
             set_mapss)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val init_ex_mor_thm =
       let
         val goal = HOLogic.mk_Trueprop

       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} =>
             mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm (alg_min_alg_thm RS copy_thm)
               card_of_min_alg_thms mor_Rep_thm mor_comp_thm mor_select_thm mor_incl_thm)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val mor_fold_thm =
       let
         val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);

         val vars = Variable.add_free_names lthy goal [];
       in
         Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, ...} =>
             mk_mor_fold_tac ctxt cT ct fold_defs init_ex_mor_thm mor_cong)
-        |> Thm.close_derivation
+        |> Thm.close_derivation \<^here>
       end;
 
     val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
       ((rtac lthy CollectI THEN' CONJ_WRAP' (K (rtac lthy @{thm subset_UNIV})) (1 upto m + n)) 1)
       (mor_fold_thm RS morE)) morE_thms;

         val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
         val vars = fold (Variable.add_free_names lthy) [prem, unique] [];
         val unique_mor = Goal.prove_sorry lthy vars [] (Logic.mk_implies (prem, unique))
           (fn {context = ctxt, prems = _} => mk_fold_unique_mor_tac ctxt type_defs
             init_unique_mor_thms Reps mor_comp_thm mor_Abs_thm mor_fold_thm)
-          |> Thm.close_derivation;
+          |> Thm.close_derivation \<^here>;
       in
         `split_conj_thm unique_mor
       end;
 
     val (ctor_fold_unique_thms, ctor_fold_unique_thm) =

       in
         @{map 5} (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L =>
           Goal.prove_sorry lthy [] [] goal
             (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt dtor_def foldx map_comp_id
               map_cong0L ctor_o_fold_thms)
-          |> Thm.close_derivation)
+          |> Thm.close_derivation \<^here>)
         goals dtor_defs ctor_fold_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;

       in
         (Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} =>
             mk_ctor_induct_tac ctxt m set_mapss init_induct_thm morE_thms mor_Abs_thm
             Rep_inverses Abs_inverses Reps)
-        |> Thm.close_derivation,
+        |> Thm.close_derivation \<^here>,
         rev (Term.add_tfrees goal []))
       end;
 
     val cTs = map (SOME o Thm.ctyp_of lthy o TFree) induct_params;
 

         val vars = Variable.add_free_names lthy goal [];
       in
         (Goal.prove_sorry lthy vars [] goal
           (fn {context = ctxt, prems = _} => mk_ctor_induct2_tac ctxt cTs cts ctor_induct_thm
             weak_ctor_induct_thms)
-        |> Thm.close_derivation,
+        |> Thm.close_derivation \<^here>,
         rev (Term.add_tfrees goal []))
       end;
 
     val timer = time (timer "induction");
 

               @{map 4} (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
                 Variable.add_free_names lthy goal []
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
                     mk_map_tac ctxt m n foldx map_comp_id map_cong0))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               goals ctor_fold_thms map_comp_id_thms map_cong0s;
           in
             `(map (fn thm => thm RS @{thm comp_eq_dest})) maps
           end;
 

                 (map2 (curry HOLogic.mk_eq) us fs_Imaps));
             val vars = fold (Variable.add_free_names lthy) (goal :: prems) [];
             val unique = Goal.prove_sorry lthy vars [] (Logic.list_implies (prems, goal))
               (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
                 mk_ctor_map_unique_tac ctxt ctor_fold_unique_thm sym_map_comps)
-              |> Thm.close_derivation;
+              |> Thm.close_derivation \<^here>;
           in
             `split_conj_thm unique
           end;
 
         val timer = time (timer "map functions for the new datatypes");

               @{map 3} (fn sets => @{map 4} (mk_goal sets) ctors sets)
                 Isetss_by_range colss map_setss;
             val setss = map (map2 (fn foldx => fn goal =>
                 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
                   unfold_thms_tac ctxt Iset_defs THEN mk_set_tac ctxt foldx)
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               ctor_fold_thms) goalss;
 
             fun mk_simp_goal pas_set act_sets sets ctor z set =
               mk_Trueprop_eq (set $ (ctor $ z),
                 mk_union (pas_set $ z,

             val ctor_setss = @{map 3} (fn i => @{map 3} (fn set_nats => fn goal => fn set =>
               Variable.add_free_names lthy goal []
               |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} =>
                     mk_ctor_set_tac ctxt set (nth set_nats (i - 1)) (drop m set_nats)))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               set_mapss) ls simp_goalss setss;
           in
             ctor_setss
           end;
 

             val thms =
               @{map 5} (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
                 Variable.add_free_names lthy goal []
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                   (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               goals csetss ctor_Iset_thmss inducts ls;
           in
             map split_conj_thm thms
           end;
 

               @{map 4} (fn goal => fn ctor_sets => fn induct => fn i =>
                 Variable.add_free_names lthy goal []
                 |> (fn vars => Goal.prove_sorry lthy vars [] goal
                     (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
                       mk_tac ctxt induct ctor_sets i))
-                |> Thm.close_derivation)
+                |> Thm.close_derivation \<^here>)
               goals ctor_Iset_thmss inducts ls;
           in
             map split_conj_thm thms
           end;
 

             val vars = Variable.add_free_names lthy goal [];
 
             val thm = Goal.prove_sorry lthy vars [] goal
                 (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac ctxt induct) set_Iset_thmsss
                   map_cong0s ctor_Imap_thms)
-              |> Thm.close_derivation;
+              |> Thm.close_derivation \<^here>;
           in
             split_conj_thm thm
           end;
 
         val in_rels = map in_rel_of_bnf bnfs;

               Variable.add_free_names lthy goal []
               |> (fn vars => Goal.prove_sorry lthy vars [] goal
                (fn {context = ctxt, prems = _} =>
                  mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
                    ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss))
-              |> Thm.close_derivation)
+              |> Thm.close_derivation \<^here>)
             ks goals in_rels map_comps map_cong0s ctor_Imap_thms ctor_Iset_thmss'
               ctor_inject_thms ctor_dtor_thms set_mapss ctor_Iset_incl_thmss
               ctor_set_Iset_incl_thmsss
           end;
 

             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 m induct ctor_nchotomy_thms
                 ctor_Irel_thms rel_mono_strong0s le_rel_OOs)
-            |> Thm.close_derivation
+            |> Thm.close_derivation \<^here>
           end;
 
         val timer = time (timer "helpers for BNF properties");
 
         val map_id0_tacs = map (fn thm => fn ctxt => mk_map_id0_tac ctxt map_id0s thm)