src/HOL/Tools/BNF/bnf_gfp.ML

             (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
         val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs';
         val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
       in
         Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
-          (K (mk_map_cong0L_tac m map_cong0 map_id))
+          (fn {context = ctxt, prems = _} => mk_map_cong0L_tac ctxt m map_cong0 map_id)
         |> Thm.close_derivation
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;

           @{map 3} (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y))
             yFs yFs_copy maps;
         val goals = map2 (fn prem => fn concl => Logic.mk_implies (prem, concl)) prems concls;
       in
         map (fn goal =>
-          Goal.prove_sorry lthy [] [] goal (K ((hyp_subst_tac lthy THEN' rtac refl) 1))
+          Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+            (hyp_subst_tac ctxt THEN' rtac ctxt refl) 1)
           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy)) goals
       end;
 
     val timer = time (timer "Derived simple theorems");

           ss zs setssAs;
         val goalss = map2 (fn prem => fn concls => map (fn concl =>
           Logic.list_implies (coalg_prem :: [prem], concl)) concls) prems conclss;
       in
         map (fn goals => map (fn goal =>
-          Goal.prove_sorry lthy [] [] goal (K (mk_coalg_set_tac coalg_def))
+          Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+            mk_coalg_set_tac ctxt coalg_def)
           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy)) goals) goalss
       end;
 
     fun mk_tcoalg BTs = mk_coalg (map HOLogic.mk_UNIV BTs);

     val tcoalg_thm =
       let
         val goal = HOLogic.mk_Trueprop (mk_tcoalg activeAs ss)
       in
         Goal.prove_sorry lthy [] [] goal
-          (K (rtac (coalg_def RS iffD2) 1 THEN CONJ_WRAP
-            (K (EVERY' [rtac ballI, rtac CollectI,
-              CONJ_WRAP' (K (EVERY' [rtac @{thm subset_UNIV}])) allAs] 1)) ss))
+          (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
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val timer = time (timer "Coalgebra definition & thms");

         fun mk_elim_goal B mapAsBs f s s' x =
           Logic.list_implies ([prem, mk_Trueprop_mem (x, B)],
             mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)));
         val elim_goals = @{map 6} mk_elim_goal Bs mapsAsBs fs ss s's zs;
         fun prove goal =
-          Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def))
+          Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+            mk_mor_elim_tac ctxt mor_def)
           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy);
       in
         (map prove image_goals, map prove elim_goals)
       end;

       let
         val prems = map2 (HOLogic.mk_Trueprop oo mk_leq) Bs Bs_copy;
         val concl = HOLogic.mk_Trueprop (mk_mor Bs ss Bs_copy ss active_ids);
       in
         Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, concl))
-          (K (mk_mor_incl_tac mor_def map_ids))
+          (fn {context = ctxt, prems = _} => mk_mor_incl_tac ctxt mor_def map_ids)
         |> Thm.close_derivation
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_id_thm = mor_incl_thm OF (replicate n subset_refl);

             HOLogic.mk_comp (s', f));
         val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
         val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's);
       in
         Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
-          (K (mk_mor_UNIV_tac morE_thms mor_def))
+          (fn {context = ctxt, prems = _} => mk_mor_UNIV_tac ctxt morE_thms mor_def)
         |> Thm.close_derivation
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_str_thm =

         val maps = map2 (fn Ds => fn bnf => Term.list_comb
           (mk_map_of_bnf Ds allAs (passiveAs @ FTsAs) bnf, passive_ids @ ss)) Dss bnfs;
       in
         Goal.prove_sorry lthy [] []
           (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss (map HOLogic.mk_UNIV FTsAs) maps ss))
-          (K (mk_mor_str_tac ks mor_UNIV_thm))
+          (fn {context = ctxt, prems = _} => mk_mor_str_tac ctxt ks mor_UNIV_thm)
         |> Thm.close_derivation
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val mor_case_sum_thm =

           mk_case_sum (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s))
           s's sum_ss map_Inls;
       in
         Goal.prove_sorry lthy [] []
           (HOLogic.mk_Trueprop (mk_mor (map HOLogic.mk_UNIV activeBs) s's sum_UNIVs maps Inls))
-          (K (mk_mor_case_sum_tac ks mor_UNIV_thm))
+          (fn {context = ctxt, prems = _} => mk_mor_case_sum_tac ctxt ks mor_UNIV_thm)
         |> Thm.close_derivation
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val timer = time (timer "Morphism definition & thms");

         val rhs = HOLogic.mk_conj
           (bis_le, Library.foldr1 HOLogic.mk_conj
             (@{map 6} mk_conjunct Rs ss s's zs z's relsAsBs))
       in
         Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs))
-          (K (mk_bis_rel_tac m bis_def in_rels map_comps map_cong0s set_mapss))
+          (fn {context = ctxt, prems = _} => mk_bis_rel_tac ctxt m bis_def in_rels map_comps
+            map_cong0s set_mapss)
         |> Thm.close_derivation
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
     val bis_converse_thm =
       Goal.prove_sorry lthy [] []
         (Logic.mk_implies (HOLogic.mk_Trueprop (mk_bis Bs ss B's s's Rs),
           HOLogic.mk_Trueprop (mk_bis B's s's Bs ss (map mk_converse Rs))))
-        (K (mk_bis_converse_tac m bis_rel_thm rel_congs rel_converseps))
+        (fn {context = ctxt, prems = _} => mk_bis_converse_tac ctxt m bis_rel_thm rel_congs
+          rel_converseps)
       |> Thm.close_derivation
       |> singleton (Proof_Context.export names_lthy lthy);
 
     val bis_O_thm =
       let

       let
         fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis Bs ss i));
         val goals = map2 (fn i => fn R => Logic.mk_implies (sbis_prem, mk_concl i R)) ks sRs;
       in
         @{map 3} (fn goal => fn i => fn def =>
-          Goal.prove_sorry lthy [] [] goal (K (mk_incl_lsbis_tac n i def))
+          Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+            mk_incl_lsbis_tac ctxt n i def)
           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy)) goals ks lsbis_defs
       end;
 
     val equiv_lsbis_thms =

         fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis Bs ss i));
         val goals = map2 (fn i => fn B => Logic.mk_implies (coalg_prem, mk_concl i B)) ks Bs;
       in
         @{map 3} (fn goal => fn l_incl => fn incl_l =>
           Goal.prove_sorry lthy [] [] goal
-            (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l
-              bis_Id_on_thm bis_converse_thm bis_O_thm))
+            (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
           |> singleton (Proof_Context.export names_lthy lthy))
         goals lsbis_incl_thms incl_lsbis_thms
       end;
 

         let
           val sbdT_bind = mk_internal_b sum_bdTN;
 
           val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
             typedef (sbdT_bind, sum_bdT_params', NoSyn)
-              (HOLogic.mk_UNIV sum_bdT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
+              (HOLogic.mk_UNIV sum_bdT) NONE (fn ctxt =>
+                EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy;
 
           val sbdT = Type (sbdT_name, sum_bdT_params);
           val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT);
 
           val sbd_bind = mk_internal_b sum_bdN;

             (mk_Trueprop_mem (kl, mk_Lev ss nat i $ z),
             mk_Trueprop_mem (kl, mk_Lev ss (mk_size kl) i $ z));
         val goals = map2 mk_goal ks zs;
 
         val length_Levs' = map2 (fn goal => fn length_Lev =>
-          Goal.prove_sorry lthy [] [] goal (K (mk_length_Lev'_tac length_Lev))
+          Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+            mk_length_Lev'_tac ctxt length_Lev)
           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy)) goals length_Levs;
       in
         (length_Levs, length_Levs')
       end;

         val cTs = [SOME (Thm.ctyp_of lthy sum_sbdT)];
         val cts = map (SOME o Thm.cterm_of lthy) [Term.absfree kl' goal, kl];
 
         val rv_last =
           Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
-            (K (mk_rv_last_tac cTs cts rv_Nils rv_Conss))
+            (fn {context = ctxt, prems = _} => mk_rv_last_tac ctxt cTs cts rv_Nils rv_Conss)
           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy);
 
         val rv_last' = mk_specN (n + 1) rv_last;
       in

 
         val goals = @{map 3} mk_goal lsbisAs final_maps strTAs;
       in
         @{map 4} (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
           Goal.prove_sorry lthy [] [] goal
-            (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBIS_thms))
+            (fn {context = ctxt, prems = _} => mk_congruent_str_final_tac ctxt m lsbisE map_comp_id
+              map_cong0 equiv_LSBIS_thms)
           |> Thm.close_derivation)
         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))
-      (K (mk_coalg_final_tac m coalg_def congruent_str_final_thms equiv_LSBIS_thms
-        set_mapss coalgT_set_thmss))
+      (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;
 
     val mor_T_final_thm = Goal.prove_sorry lthy [] []
       (HOLogic.mk_Trueprop (mk_mor carTAs strTAs car_finals str_finals (map mk_proj lsbisAs)))
-      (K (mk_mor_T_final_tac mor_def congruent_str_final_thms equiv_LSBIS_thms))
+      (fn {context = ctxt, prems = _} => mk_mor_T_final_tac ctxt 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 thm => thm OF [mor_final_thm, UNIV_I]) mor_image'_thms;
 
     val timer = time (timer "Final coalgebra");
 
     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
       lthy
       |> @{fold_map 4} (fn b => fn mx => fn car_final => fn in_car_final =>
-        typedef (b, params, mx) car_final NONE
-          (fn _ => EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
+          typedef (b, params, mx) car_final NONE
+            (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt in_car_final] 1))
+        bs mixfixes car_finals in_car_final_thms
       |>> apsnd split_list o split_list;
 
     val Ts = map (fn name => Type (name, params')) T_names;
     fun mk_Ts passive = map (Term.typ_subst_atomic (passiveAs ~~ passive)) Ts;
     val Ts' = mk_Ts passiveBs;

         val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
         val morEs' = map (fn thm => (thm OF [mor_final_thm, UNIV_I]) RS sym) morE_thms;
       in
         Goal.prove_sorry lthy [] []
           (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks)))
-          (K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs'
-            map_comp_id_thms map_cong0s))
+          (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
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
     val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
 

         val prem = HOLogic.mk_Trueprop (mk_sbis UNIVs dtors TRs);
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
           (map2 (fn R => fn T => mk_leq R (Id_const T)) TRs Ts));
       in
         `split_conj_thm (Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, concl))
-          (K (mk_raw_coind_tac bis_def bis_cong_thm bis_O_thm bis_converse_thm bis_Gr_thm
-            tcoalg_thm coalgT_thm mor_T_final_thm sbis_lsbis_thm
-            lsbis_incl_thms incl_lsbis_thms equiv_LSBIS_thms mor_Rep_thm Rep_injects))
+          (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
           |> singleton (Proof_Context.export names_lthy lthy))
       end;
 
     val (unfold_unique_mor_thms, unfold_unique_mor_thm) =

 
         val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
         val mor_thm = mor_comp_thm OF [mor_final_thm, mor_Abs_thm];
 
         val unique_mor = Goal.prove_sorry lthy [] [] (Logic.mk_implies (prem, unique))
-          (K (mk_unfold_unique_mor_tac raw_coind_thms bis_thm mor_thm unfold_defs))
+          (fn {context = ctxt, prems = _} => mk_unfold_unique_mor_tac ctxt raw_coind_thms
+            bis_thm mor_thm unfold_defs)
           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy);
       in
         `split_conj_thm unique_mor
       end;

         val rel_prems = @{map 5} mk_rel_prem phis dtors rels Jzs Jzs_copy;
         val dtor_coinduct_goal = Logic.list_implies (rel_prems, concl);
 
         val dtor_coinduct =
           Goal.prove_sorry lthy [] [] dtor_coinduct_goal
-            (K (mk_dtor_coinduct_tac m raw_coind_thm bis_rel_thm rel_congs))
+            (fn {context = ctxt, prems = _} => mk_dtor_coinduct_tac ctxt m raw_coind_thm bis_rel_thm
+              rel_congs)
           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy);
       in
         (rev (Term.add_tfrees dtor_coinduct_goal []), dtor_coinduct)
       end;

 
     fun mk_Jrel_DEADID_coinduct_thm () =
       mk_xtor_rel_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
         Jzs Jz's dtors dtor's (fn {context = ctxt, prems} =>
           (unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
-          REPEAT_DETERM (rtac allI 1) THEN rtac (dtor_coinduct_thm OF prems) 1)) lthy;
+          REPEAT_DETERM (rtac ctxt allI 1) THEN rtac ctxt (dtor_coinduct_thm OF prems) 1)) lthy;
 
     (*register new codatatypes as BNFs*)
     val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jmap_unique_thms, dtor_Jset_thmss',
       dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, dtor_Jset_induct_thms, lthy) =
       if m = 0 then

             val goals = @{map 4} mk_goal fs_Jmaps map_FTFT's dtors dtor's;
             val maps =
               @{map 5} (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong =>
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
-                     mk_map_tac m n map_arg_cong unfold map_comp map_cong0)
+                     mk_map_tac ctxt m n map_arg_cong unfold map_comp map_cong0)
                 |> Thm.close_derivation
                 |> singleton (Proof_Context.export names_lthy lthy))
               goals dtor_unfold_thms map_comps map_cong0s map_arg_cong_thms;
           in
             map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps

               (@{map 3} (fn fmap => fn gmap => fn fgmap =>
                  HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
               fs_Jmaps gs_Jmaps fgs_Jmaps))
           in
             split_conj_thm (Goal.prove_sorry lthy [] [] goal
-              (K (mk_map_comp0_tac Jmap_thms map_comp0s dtor_Jmap_unique_thm))
+              (fn {context = ctxt, prems = _} =>
+                mk_map_comp0_tac ctxt Jmap_thms map_comp0s dtor_Jmap_unique_thm)
               |> Thm.close_derivation
               |> singleton (Proof_Context.export names_lthy lthy))
           end;
 
         val timer = time (timer "map functions for the new codatatypes");

           in
             (map2 (fn goals => fn rec_Sucs =>
               map2 (fn goal => fn rec_Suc =>
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
-                    mk_set_incl_Jset_tac rec_Suc)
+                    mk_set_incl_Jset_tac ctxt rec_Suc)
                 |> Thm.close_derivation
                 |> singleton (Proof_Context.export names_lthy lthy))
               goals rec_Sucs)
             set_incl_Jset_goalss col_Sucss,
             map2 (fn goalss => fn rec_Sucs =>
               map2 (fn k => fn goals =>
                 map2 (fn goal => fn rec_Suc =>
                   Goal.prove_sorry lthy [] [] goal
                     (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
-                      mk_set_Jset_incl_Jset_tac n rec_Suc k)
+                      mk_set_Jset_incl_Jset_tac ctxt n rec_Suc k)
                   |> Thm.close_derivation
                   |> singleton (Proof_Context.export names_lthy lthy))
                 goals rec_Sucs)
               ks goalss)
             set_Jset_incl_Jset_goalsss col_Sucss)

                 |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y')
                 |> unfold_thms lthy incls) OF
                 (replicate n ballI @
                   maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
               |> singleton (Proof_Context.export names_lthy lthy)
-              |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl)))
+              |> rule_by_tactic lthy (ALLGOALS (TRY o etac lthy asm_rl)))
             Jset_minimal_thms set_Jset_incl_Jset_thmsss' Jsetss_by_range ys ys' dtor_set_induct_phiss
           end;
 
         val (dtor_Jset_thmss', dtor_Jset_thmss) =
           let

             val le_goals = map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
               (mk_goals (uncurry mk_leq));
             val set_le_thmss = map split_conj_thm
               (@{map 4} (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss =>
                 Goal.prove_sorry lthy [] [] goal
-                  (K (mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss))
+                  (fn {context = ctxt, prems = _} =>
+                    mk_set_le_tac ctxt n Jset_minimal set_Jsets set_Jset_Jsetss)
                 |> Thm.close_derivation
                 |> singleton (Proof_Context.export names_lthy lthy))
               le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss');
 
             val ge_goalss = map (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 =>
                 Goal.prove_sorry lthy [] [] goal
-                  (K (mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets))
+                  (fn {context = ctxt, prems = _} =>
+                    mk_set_ge_tac ctxt n set_incl_Jset set_Jset_incl_Jsets)
                 |> Thm.close_derivation
                 |> singleton (Proof_Context.export names_lthy lthy)))
               ge_goalss set_incl_Jset_thmss' set_Jset_incl_Jset_thmsss'
           in
             map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss

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

               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                 (@{map 4} mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps));
 
             val thm =
               Goal.prove_sorry lthy [] [] goal
-                (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s
-                  set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels))
+                (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
               |>  singleton (Proof_Context.export names_lthy lthy);
           in
             split_conj_thm thm
           end;

               mk_leq (mk_rel_compp (Jrelpsi1, Jrelpsi2)) Jrelpsi12;
             val goals = @{map 3} mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s;
 
             val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
           in
-            Goal.prove_sorry lthy [] [] goal
-              (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms le_rel_OOs))
+            Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+              mk_le_rel_OO_tac ctxt Jrel_coinduct_thm dtor_Jrel_thms le_rel_OOs)
             |> Thm.close_derivation
             |> singleton (Proof_Context.export names_lthy lthy)
           end;
 
         val timer = time (timer "helpers for BNF properties");

           |> split_list;
 
         val timer = time (timer "witnesses");
 
         val map_id0_tacs =
-          map2 (K oo mk_map_id0_tac Jmap_thms) dtor_unfold_unique_thms unfold_dtor_thms;
-        val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms;
+          map2 (fn thm => fn thm' => fn ctxt =>
+            mk_map_id0_tac ctxt Jmap_thms thm thm')
+          dtor_unfold_unique_thms unfold_dtor_thms;
+        val map_comp0_tacs = map (fn thm => fn ctxt => rtac ctxt (thm RS sym) 1) Jmap_comp0_thms;
         val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) map_cong0_thms;
         val set_map0_tacss =
-          map (map (fn col => fn ctxt => unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac col))
-            (transpose col_natural_thmss);
+          map (map (fn col => fn ctxt =>
+            unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac ctxt col))
+          (transpose col_natural_thmss);
 
         val Jbd_card_orders = map (fn def => fold_thms lthy [def] sbd_card_order) Jbd_defs;
         val Jbd_Cinfinites = map (fn def => fold_thms lthy [def] sbd_Cinfinite) Jbd_defs;
 
-        val bd_co_tacs = map (fn thm => K (rtac thm 1)) Jbd_card_orders;
-        val bd_cinf_tacs = map (fn thm => K (rtac (thm RS conjunct1) 1)) Jbd_Cinfinites;
+        val bd_co_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) Jbd_card_orders;
+        val bd_cinf_tacs = map (fn thm => fn ctxt => rtac ctxt (thm RS conjunct1) 1) Jbd_Cinfinites;
 
         val set_bd_tacss =
           map2 (fn Cinf => map (fn col => fn ctxt =>
-            unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac Cinf col))
+            unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac ctxt Cinf col))
           Jbd_Cinfinites (transpose col_bd_thmss);
 
-        val le_rel_OO_tacs = map (fn i => K (rtac (le_Jrel_OO_thm RS mk_conjunctN n i) 1)) ks;
-
-        val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Jrel_unabs_defs;
+        val le_rel_OO_tacs = map (fn i => fn ctxt =>
+          rtac ctxt (le_Jrel_OO_thm RS mk_conjunctN n i) 1) ks;
+
+        val rel_OO_Grp_tacs = map (fn def => fn ctxt => rtac ctxt def 1) Jrel_unabs_defs;
 
         val tacss = @{map 9} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
 
         fun wit_tac thms ctxt =