src/HOL/HOLCF/Tools/Domain/domain_constructors.ML

           val eqn = mk_eq (y, list_ccomb (con, vs))
           val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy)
         in Library.foldr mk_ex (vs, conj) end
       val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
       (* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
-      fun tacs {context = ctxt, prems} = [
+      fun tacs ctxt = [
           rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
           rewrite_goals_tac ctxt [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
           rtac thm3 1]
     in
-      val nchotomy = prove thy con_betas goal tacs
+      val nchotomy = prove thy con_betas goal (tacs o #context)
       val exhaust =
           (nchotomy RS @{thm exh_casedist0})
           |> rewrite_rule (Proof_Context.init_global thy) @{thms exh_casedists}
           |> Drule.zero_var_indexes
     end

           fun one_strict v' =
             let
               val bottom = mk_bottom (fastype_of v')
               val vs' = map (fn v => if v = v' then bottom else v) vs
               val goal = mk_trp (mk_undef (list_ccomb (con, vs')))
-              val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
-            in prove thy con_betas goal (K tacs) end
+              fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
+            in prove thy con_betas goal (tacs o #context) end
         in map one_strict nonlazy end
 
       fun con_defin (con, args) =
         let
           fun iff_disj (t, []) = HOLogic.mk_not t

           val lhs = mk_undef (list_ccomb (con, vs))
           val rhss = map mk_undef nonlazy
           val goal = mk_trp (iff_disj (lhs, rhss))
           val rule1 = iso_locale RS @{thm iso.abs_bottom_iff}
           val rules = rule1 :: @{thms con_bottom_iff_rules}
-          val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
-        in prove thy con_betas goal (K tacs) end
+          fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
+        in prove thy con_betas goal (tacs o #context) end
     in
       val con_stricts = maps con_strict spec'
       val con_defins = map con_defin spec'
       val con_rews = con_stricts @ con_defins
     end

         let
           val abs_below = iso_locale RS @{thm iso.abs_below}
           val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below}
           val rules2 = @{thms up_defined spair_defined ONE_defined}
           val rules = rules1 @ rules2
-          val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
-        in map (fn c => pgterm mk_below c (K tacs)) cons' end
+          fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
+        in map (fn c => pgterm mk_below c (tacs o #context)) cons' end
       val injects =
         let
           val abs_eq = iso_locale RS @{thm iso.abs_eq}
           val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq}
           val rules2 = @{thms up_defined spair_defined ONE_defined}
           val rules = rules1 @ rules2
-          val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
-        in map (fn c => pgterm mk_eq c (K tacs)) cons' end
+          fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
+        in map (fn c => pgterm mk_eq c (tacs o #context)) cons' end
     end
 
     (* prove distinctness of constructors *)
     local
       fun map_dist (f : 'a -> 'a -> 'b) (xs : 'a list) : 'b list =

           val lhs = mk_below (list_ccomb (con1, vs1), list_ccomb (con2, vs2))
           val rhss = map mk_undef zs1
           val goal = mk_trp (iff_disj (lhs, rhss))
           val rule1 = iso_locale RS @{thm iso.abs_below}
           val rules = rule1 :: @{thms con_below_iff_rules}
-          val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
-        in prove thy con_betas goal (K tacs) end
+          fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
+        in prove thy con_betas goal (tacs o #context) end
       fun dist_eq (con1, args1) (con2, args2) =
         let
           val (vs1, zs1) = get_vars args1
           val (vs2, zs2) = get_vars args2 |> pairself (map prime)
           val lhs = mk_eq (list_ccomb (con1, vs1), list_ccomb (con2, vs2))
           val rhss1 = map mk_undef zs1
           val rhss2 = map mk_undef zs2
           val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2))
           val rule1 = iso_locale RS @{thm iso.abs_eq}
           val rules = rule1 :: @{thms con_eq_iff_rules}
-          val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
-        in prove thy con_betas goal (K tacs) end
+          fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
+        in prove thy con_betas goal (tacs o #context) end
     in
       val dist_les = map_dist dist_le spec'
       val dist_eqs = map_dist dist_eq spec'
     end
 

           val defs = case_beta :: con_betas
           val rules1 = @{thms strictify2 sscase2 sscase3 ssplit2 fup2 ID1}
           val rules2 = @{thms con_bottom_iff_rules}
           val rules3 = @{thms cfcomp2 one_case2}
           val rules = abs_inverse :: rules1 @ rules2 @ rules3
-          val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1]
-        in prove thy defs goal (K tacs) end
+          fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps rules) 1]
+        in prove thy defs goal (tacs o #context) end
     in
       val case_apps = map2 one_case spec fs
     end
 
   in

 
     (* prove selector strictness rules *)
     val sel_stricts : thm list =
       let
         val rules = rep_strict :: @{thms sel_strict_rules}
-        val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
+        fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
         fun sel_strict sel =
           let
             val goal = mk_trp (mk_strict sel)
           in
-            prove thy sel_defs goal (K tacs)
+            prove thy sel_defs goal (tacs o #context)
           end
       in
         map sel_strict sel_consts
       end
 
     (* prove selector application rules *)
     val sel_apps : thm list =
       let
         val defs = con_betas @ sel_defs
         val rules = abs_inv :: @{thms sel_app_rules}
-        val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
+        fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
         fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) =
           let
             val Ts : typ list = map #3 args
             val ns : string list = Datatype_Prop.make_tnames Ts
             val vs : term list = map Free (ns ~~ Ts)

                 val xs = map snd (filter_out fst (nth_drop n vs'))
                 val assms = map (mk_trp o mk_defined) xs
                 val concl = mk_trp (mk_eq (sel ` con_app, nth vs n))
                 val goal = Logic.list_implies (assms, concl)
               in
-                prove thy defs goal (K tacs)
+                prove thy defs goal (tacs o #context)
               end
             fun one_diff (_, sel, T) =
               let
                 val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T))
               in
-                prove thy defs goal (K tacs)
+                prove thy defs goal (tacs o #context)
               end
             fun one_con (j, (_, args')) : thm list =
               let
                 fun prep (_, (_, NONE, _)) = NONE
                   | prep (i, (_, SOME sel, T)) = SOME (i, sel, T)

 
   (* prove selector definedness rules *)
     val sel_defins : thm list =
       let
         val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules}
-        val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
+        fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
         fun sel_defin sel =
           let
             val (T, U) = dest_cfunT (fastype_of sel)
             val x = Free ("x", T)
             val lhs = mk_eq (sel ` x, mk_bottom U)
             val rhs = mk_eq (x, mk_bottom T)
             val goal = mk_trp (mk_eq (lhs, rhs))
           in
-            prove thy sel_defs goal (K tacs)
+            prove thy sel_defs goal (tacs o #context)
           end
         fun one_arg (false, SOME sel, _) = SOME (sel_defin sel)
           | one_arg _                    = NONE
       in
         case spec2 of

           val lhs = dis ` list_ccomb (con, vs)
           val rhs = if i = j then @{term TT} else @{term FF}
           val assms = map (mk_trp o mk_defined) nonlazy
           val concl = mk_trp (mk_eq (lhs, rhs))
           val goal = Logic.list_implies (assms, concl)
-          val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
-        in prove thy dis_defs goal (K tacs) end
+          fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
+        in prove thy dis_defs goal (tacs o #context) end
       fun one_dis (i, dis) =
           map_index (dis_app (i, dis)) spec
     in
       val dis_apps = flat (map_index one_dis dis_consts)
     end

     local
       fun dis_defin dis =
         let
           val x = Free ("x", lhsT)
           val simps = dis_apps @ @{thms dist_eq_tr}
-          val tacs =
+          fun tacs ctxt =
             [rtac @{thm iffI} 1,
-             asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps dis_stricts) 2,
+             asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps dis_stricts) 2,
              rtac exhaust 1, atac 1,
-             ALLGOALS (asm_full_simp_tac (Simplifier.global_context thy simple_ss addsimps simps))]
+             ALLGOALS (asm_full_simp_tac (put_simpset simple_ss ctxt addsimps simps))]
           val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x))
-        in prove thy [] goal (K tacs) end
+        in prove thy [] goal (tacs o #context) end
     in
       val dis_defins = map dis_defin dis_consts
     end
 
   in

       fun match_strict mat =
         let
           val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat))
           val k = Free ("k", U)
           val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V))
-          val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
-        in prove thy match_defs goal (K tacs) end
+          fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
+        in prove thy match_defs goal (tacs o #context) end
     in
       val match_stricts = map match_strict match_consts
     end
 
     (* prove match/constructor rules *)

           val lhs = mat ` list_ccomb (con, vs) ` k
           val rhs = if i = j then list_ccomb (k, vs) else fail
           val assms = map (mk_trp o mk_defined) nonlazy
           val concl = mk_trp (mk_eq (lhs, rhs))
           val goal = Logic.list_implies (assms, concl)
-          val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
-        in prove thy match_defs goal (K tacs) end
+          fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
+        in prove thy match_defs goal (tacs o #context) end
       fun one_match (i, mat) =
           map_index (match_app (i, mat)) spec
     in
       val match_apps = flat (map_index one_match match_consts)
     end