src/HOL/HOLCF/ex/Pattern_Match.thy

         let
           val (fun1, fun2, taken) = pat_lhs (pat, args);
           val defs = @{thm branch_def} :: pat_defs;
           val goal = mk_trp (mk_strict fun1);
           val rules = @{thms match_bind_simps} @ case_rews;
-          val tacs = [simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1];
-        in prove thy defs goal (K tacs) end;
+          fun tacs ctxt = [simp_tac (put_simpset beta_ss ctxt addsimps rules) 1];
+        in prove thy defs goal (tacs o #context) end;
       fun pat_apps (i, (pat, (con, args))) =
         let
           val (fun1, fun2, taken) = pat_lhs (pat, args);
           fun pat_app (j, (con', args')) =
             let

               val rhs = if i = j then fun2 ` mk_tuple vs else mk_fail R;
               val concl = mk_trp (mk_eq (fun1 ` con_app, rhs));
               val goal = Logic.list_implies (assms, concl);
               val defs = @{thm branch_def} :: pat_defs;
               val rules = @{thms match_bind_simps} @ case_rews;
-              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 map_index pat_app spec end;
     in
       val pat_stricts = map pat_strict (pat_consts ~~ spec);
       val pat_apps = flat (map_index pat_apps (pat_consts ~~ spec));
     end;