clarified simplifier context;
authorwenzelm
Wed Jan 01 14:29:22 2014 +0100 (2014-01-01)
changeset 54895515630483010
parent 54894 cb9d981fa9a0
child 54896 f6f455df1034
clarified simplifier context;
eliminated Simplifier.global_context;
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/record.ML
src/Pure/raw_simplifier.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_simp.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Jan 01 13:24:23 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Jan 01 14:29:22 2014 +0100
     1.3 @@ -227,12 +227,12 @@
     1.4          in Library.foldr mk_ex (vs, conj) end
     1.5        val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
     1.6        (* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
     1.7 -      fun tacs {context = ctxt, prems} = [
     1.8 +      fun tacs ctxt = [
     1.9            rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
    1.10            rewrite_goals_tac ctxt [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
    1.11            rtac thm3 1]
    1.12      in
    1.13 -      val nchotomy = prove thy con_betas goal tacs
    1.14 +      val nchotomy = prove thy con_betas goal (tacs o #context)
    1.15        val exhaust =
    1.16            (nchotomy RS @{thm exh_casedist0})
    1.17            |> rewrite_rule (Proof_Context.init_global thy) @{thms exh_casedists}
    1.18 @@ -272,8 +272,8 @@
    1.19                val bottom = mk_bottom (fastype_of v')
    1.20                val vs' = map (fn v => if v = v' then bottom else v) vs
    1.21                val goal = mk_trp (mk_undef (list_ccomb (con, vs')))
    1.22 -              val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
    1.23 -            in prove thy con_betas goal (K tacs) end
    1.24 +              fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
    1.25 +            in prove thy con_betas goal (tacs o #context) end
    1.26          in map one_strict nonlazy end
    1.27  
    1.28        fun con_defin (con, args) =
    1.29 @@ -286,8 +286,8 @@
    1.30            val goal = mk_trp (iff_disj (lhs, rhss))
    1.31            val rule1 = iso_locale RS @{thm iso.abs_bottom_iff}
    1.32            val rules = rule1 :: @{thms con_bottom_iff_rules}
    1.33 -          val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
    1.34 -        in prove thy con_betas goal (K tacs) end
    1.35 +          fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
    1.36 +        in prove thy con_betas goal (tacs o #context) end
    1.37      in
    1.38        val con_stricts = maps con_strict spec'
    1.39        val con_defins = map con_defin spec'
    1.40 @@ -317,16 +317,16 @@
    1.41            val rules1 = abs_below :: @{thms sinl_below sinr_below spair_below up_below}
    1.42            val rules2 = @{thms up_defined spair_defined ONE_defined}
    1.43            val rules = rules1 @ rules2
    1.44 -          val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
    1.45 -        in map (fn c => pgterm mk_below c (K tacs)) cons' end
    1.46 +          fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
    1.47 +        in map (fn c => pgterm mk_below c (tacs o #context)) cons' end
    1.48        val injects =
    1.49          let
    1.50            val abs_eq = iso_locale RS @{thm iso.abs_eq}
    1.51            val rules1 = abs_eq :: @{thms sinl_eq sinr_eq spair_eq up_eq}
    1.52            val rules2 = @{thms up_defined spair_defined ONE_defined}
    1.53            val rules = rules1 @ rules2
    1.54 -          val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
    1.55 -        in map (fn c => pgterm mk_eq c (K tacs)) cons' end
    1.56 +          fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
    1.57 +        in map (fn c => pgterm mk_eq c (tacs o #context)) cons' end
    1.58      end
    1.59  
    1.60      (* prove distinctness of constructors *)
    1.61 @@ -350,8 +350,8 @@
    1.62            val goal = mk_trp (iff_disj (lhs, rhss))
    1.63            val rule1 = iso_locale RS @{thm iso.abs_below}
    1.64            val rules = rule1 :: @{thms con_below_iff_rules}
    1.65 -          val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
    1.66 -        in prove thy con_betas goal (K tacs) end
    1.67 +          fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
    1.68 +        in prove thy con_betas goal (tacs o #context) end
    1.69        fun dist_eq (con1, args1) (con2, args2) =
    1.70          let
    1.71            val (vs1, zs1) = get_vars args1
    1.72 @@ -362,8 +362,8 @@
    1.73            val goal = mk_trp (iff_disj2 (lhs, rhss1, rhss2))
    1.74            val rule1 = iso_locale RS @{thm iso.abs_eq}
    1.75            val rules = rule1 :: @{thms con_eq_iff_rules}
    1.76 -          val tacs = [simp_tac (Simplifier.global_context thy HOL_ss addsimps rules) 1]
    1.77 -        in prove thy con_betas goal (K tacs) end
    1.78 +          fun tacs ctxt = [simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1]
    1.79 +        in prove thy con_betas goal (tacs o #context) end
    1.80      in
    1.81        val dist_les = map_dist dist_le spec'
    1.82        val dist_eqs = map_dist dist_eq spec'
    1.83 @@ -518,8 +518,8 @@
    1.84            val rules2 = @{thms con_bottom_iff_rules}
    1.85            val rules3 = @{thms cfcomp2 one_case2}
    1.86            val rules = abs_inverse :: rules1 @ rules2 @ rules3
    1.87 -          val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1]
    1.88 -        in prove thy defs goal (K tacs) end
    1.89 +          fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps rules) 1]
    1.90 +        in prove thy defs goal (tacs o #context) end
    1.91      in
    1.92        val case_apps = map2 one_case spec fs
    1.93      end
    1.94 @@ -586,12 +586,12 @@
    1.95      val sel_stricts : thm list =
    1.96        let
    1.97          val rules = rep_strict :: @{thms sel_strict_rules}
    1.98 -        val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
    1.99 +        fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
   1.100          fun sel_strict sel =
   1.101            let
   1.102              val goal = mk_trp (mk_strict sel)
   1.103            in
   1.104 -            prove thy sel_defs goal (K tacs)
   1.105 +            prove thy sel_defs goal (tacs o #context)
   1.106            end
   1.107        in
   1.108          map sel_strict sel_consts
   1.109 @@ -602,7 +602,7 @@
   1.110        let
   1.111          val defs = con_betas @ sel_defs
   1.112          val rules = abs_inv :: @{thms sel_app_rules}
   1.113 -        val tacs = [asm_simp_tac (Simplifier.global_context thy simple_ss addsimps rules) 1]
   1.114 +        fun tacs ctxt = [asm_simp_tac (put_simpset simple_ss ctxt addsimps rules) 1]
   1.115          fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) =
   1.116            let
   1.117              val Ts : typ list = map #3 args
   1.118 @@ -617,13 +617,13 @@
   1.119                  val concl = mk_trp (mk_eq (sel ` con_app, nth vs n))
   1.120                  val goal = Logic.list_implies (assms, concl)
   1.121                in
   1.122 -                prove thy defs goal (K tacs)
   1.123 +                prove thy defs goal (tacs o #context)
   1.124                end
   1.125              fun one_diff (_, sel, T) =
   1.126                let
   1.127                  val goal = mk_trp (mk_eq (sel ` con_app, mk_bottom T))
   1.128                in
   1.129 -                prove thy defs goal (K tacs)
   1.130 +                prove thy defs goal (tacs o #context)
   1.131                end
   1.132              fun one_con (j, (_, args')) : thm list =
   1.133                let
   1.134 @@ -647,7 +647,7 @@
   1.135      val sel_defins : thm list =
   1.136        let
   1.137          val rules = rep_bottom_iff :: @{thms sel_bottom_iff_rules}
   1.138 -        val tacs = [simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1]
   1.139 +        fun tacs ctxt = [simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1]
   1.140          fun sel_defin sel =
   1.141            let
   1.142              val (T, U) = dest_cfunT (fastype_of sel)
   1.143 @@ -656,7 +656,7 @@
   1.144              val rhs = mk_eq (x, mk_bottom T)
   1.145              val goal = mk_trp (mk_eq (lhs, rhs))
   1.146            in
   1.147 -            prove thy sel_defs goal (K tacs)
   1.148 +            prove thy sel_defs goal (tacs o #context)
   1.149            end
   1.150          fun one_arg (false, SOME sel, _) = SOME (sel_defin sel)
   1.151            | one_arg _                    = NONE
   1.152 @@ -724,8 +724,8 @@
   1.153            val assms = map (mk_trp o mk_defined) nonlazy
   1.154            val concl = mk_trp (mk_eq (lhs, rhs))
   1.155            val goal = Logic.list_implies (assms, concl)
   1.156 -          val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
   1.157 -        in prove thy dis_defs goal (K tacs) end
   1.158 +          fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
   1.159 +        in prove thy dis_defs goal (tacs o #context) end
   1.160        fun one_dis (i, dis) =
   1.161            map_index (dis_app (i, dis)) spec
   1.162      in
   1.163 @@ -738,13 +738,13 @@
   1.164          let
   1.165            val x = Free ("x", lhsT)
   1.166            val simps = dis_apps @ @{thms dist_eq_tr}
   1.167 -          val tacs =
   1.168 +          fun tacs ctxt =
   1.169              [rtac @{thm iffI} 1,
   1.170 -             asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps dis_stricts) 2,
   1.171 +             asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps dis_stricts) 2,
   1.172               rtac exhaust 1, atac 1,
   1.173 -             ALLGOALS (asm_full_simp_tac (Simplifier.global_context thy simple_ss addsimps simps))]
   1.174 +             ALLGOALS (asm_full_simp_tac (put_simpset simple_ss ctxt addsimps simps))]
   1.175            val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x))
   1.176 -        in prove thy [] goal (K tacs) end
   1.177 +        in prove thy [] goal (tacs o #context) end
   1.178      in
   1.179        val dis_defins = map dis_defin dis_consts
   1.180      end
   1.181 @@ -813,8 +813,8 @@
   1.182            val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of mat))
   1.183            val k = Free ("k", U)
   1.184            val goal = mk_trp (mk_eq (mat ` mk_bottom T ` k, mk_bottom V))
   1.185 -          val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
   1.186 -        in prove thy match_defs goal (K tacs) end
   1.187 +          fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
   1.188 +        in prove thy match_defs goal (tacs o #context) end
   1.189      in
   1.190        val match_stricts = map match_strict match_consts
   1.191      end
   1.192 @@ -832,8 +832,8 @@
   1.193            val assms = map (mk_trp o mk_defined) nonlazy
   1.194            val concl = mk_trp (mk_eq (lhs, rhs))
   1.195            val goal = Logic.list_implies (assms, concl)
   1.196 -          val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps case_rews) 1]
   1.197 -        in prove thy match_defs goal (K tacs) end
   1.198 +          fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps case_rews) 1]
   1.199 +        in prove thy match_defs goal (tacs o #context) end
   1.200        fun one_match (i, mat) =
   1.201            map_index (match_app (i, mat)) spec
   1.202      in
     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Wed Jan 01 13:24:23 2014 +0100
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Wed Jan 01 14:29:22 2014 +0100
     2.3 @@ -71,9 +71,9 @@
     2.4            val rules =
     2.5                [abs_inverse] @ con_betas @ @{thms take_con_rules}
     2.6                @ take_Suc_thms @ deflation_thms @ deflation_take_thms
     2.7 -          val tac = simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1
     2.8 +          fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1
     2.9          in
    2.10 -          Goal.prove_global thy [] [] goal (K tac)
    2.11 +          Goal.prove_global thy [] [] goal (tac o #context)
    2.12          end
    2.13        val take_apps = map prove_take_app con_specs
    2.14      in
     3.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Jan 01 13:24:23 2014 +0100
     3.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Jan 01 14:29:22 2014 +0100
     3.3 @@ -158,7 +158,7 @@
     3.4      fun prove_proj (lhs, rhs) =
     3.5        let
     3.6          fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN
     3.7 -          (simp_tac (Simplifier.global_context thy beta_ss)) 1
     3.8 +          (simp_tac (put_simpset beta_ss ctxt)) 1
     3.9          val goal = Logic.mk_equals (lhs, rhs)
    3.10        in Goal.prove_global thy [] [] goal (tac o #context) end
    3.11      val proj_thms = map prove_proj projs
     4.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Jan 01 13:24:23 2014 +0100
     4.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Wed Jan 01 14:29:22 2014 +0100
     4.3 @@ -273,8 +273,8 @@
     4.4        let
     4.5          val goal = mk_trp (mk_chain take_const)
     4.6          val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd}
     4.7 -        val tac = simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1
     4.8 -        val thm = Goal.prove_global thy [] [] goal (K tac)
     4.9 +        fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1
    4.10 +        val thm = Goal.prove_global thy [] [] goal (tac o #context)
    4.11        in
    4.12          add_qualified_simp_thm "chain_take" (dbind, thm) thy
    4.13        end
    4.14 @@ -287,8 +287,8 @@
    4.15          val lhs = take_const $ @{term "0::nat"}
    4.16          val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT))
    4.17          val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict}
    4.18 -        val tac = simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1
    4.19 -        val take_0_thm = Goal.prove_global thy [] [] goal (K tac)
    4.20 +        fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1
    4.21 +        val take_0_thm = Goal.prove_global thy [] [] goal (tac o #context)
    4.22        in
    4.23          add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy
    4.24        end
    4.25 @@ -307,8 +307,8 @@
    4.26          val goal = mk_eqs (lhs, rhs)
    4.27          val simps = @{thms iterate_Suc fst_conv snd_conv}
    4.28          val rules = take_defs @ simps
    4.29 -        val tac = simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1
    4.30 -        val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac)
    4.31 +        fun tac ctxt = simp_tac (put_simpset beta_ss ctxt addsimps rules) 1
    4.32 +        val take_Suc_thm = Goal.prove_global thy [] [] goal (tac o #context)
    4.33        in
    4.34          add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy
    4.35        end
    4.36 @@ -330,11 +330,11 @@
    4.37            @ deflation_abs_rep_thms
    4.38            @ get_deflation_thms thy
    4.39        in
    4.40 -        Goal.prove_global thy [] [] goal (fn _ =>
    4.41 +        Goal.prove_global thy [] [] goal (fn {context = ctxt, ...} =>
    4.42           EVERY
    4.43            [rtac @{thm nat.induct} 1,
    4.44 -           simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps bottom_rules) 1,
    4.45 -           asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps take_Suc_thms) 1,
    4.46 +           simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1,
    4.47 +           asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps take_Suc_thms) 1,
    4.48             REPEAT (etac @{thm conjE} 1
    4.49                     ORELSE resolve_tac deflation_rules 1
    4.50                     ORELSE atac 1)])
    4.51 @@ -455,11 +455,11 @@
    4.52          val rules1 =
    4.53              take_Suc_thms @ decisive_abs_rep_thms
    4.54              @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map}
    4.55 -        val tac = EVERY [
    4.56 +        fun tac ctxt = EVERY [
    4.57              rtac @{thm nat.induct} 1,
    4.58 -            simp_tac (Simplifier.global_context thy HOL_ss addsimps rules0) 1,
    4.59 -            asm_simp_tac (Simplifier.global_context thy HOL_ss addsimps rules1) 1]
    4.60 -      in Goal.prove_global thy [] [] goal (K tac) end
    4.61 +            simp_tac (put_simpset HOL_ss ctxt addsimps rules0) 1,
    4.62 +            asm_simp_tac (put_simpset HOL_ss ctxt addsimps rules1) 1]
    4.63 +      in Goal.prove_global thy [] [] goal (tac o #context) end
    4.64      fun conjuncts 1 thm = [thm]
    4.65        | conjuncts n thm = let
    4.66            val thmL = thm RS @{thm conjunct1}
     5.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Jan 01 13:24:23 2014 +0100
     5.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Jan 01 14:29:22 2014 +0100
     5.3 @@ -558,8 +558,8 @@
     5.4            val defs = @{thm branch_def} :: pat_defs;
     5.5            val goal = mk_trp (mk_strict fun1);
     5.6            val rules = @{thms match_bind_simps} @ case_rews;
     5.7 -          val tacs = [simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1];
     5.8 -        in prove thy defs goal (K tacs) end;
     5.9 +          fun tacs ctxt = [simp_tac (put_simpset beta_ss ctxt addsimps rules) 1];
    5.10 +        in prove thy defs goal (tacs o #context) end;
    5.11        fun pat_apps (i, (pat, (con, args))) =
    5.12          let
    5.13            val (fun1, fun2, taken) = pat_lhs (pat, args);
    5.14 @@ -573,8 +573,8 @@
    5.15                val goal = Logic.list_implies (assms, concl);
    5.16                val defs = @{thm branch_def} :: pat_defs;
    5.17                val rules = @{thms match_bind_simps} @ case_rews;
    5.18 -              val tacs = [asm_simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1];
    5.19 -            in prove thy defs goal (K tacs) end;
    5.20 +              fun tacs ctxt = [asm_simp_tac (put_simpset beta_ss ctxt addsimps rules) 1];
    5.21 +            in prove thy defs goal (tacs o #context) end;
    5.22          in map_index pat_app spec end;
    5.23      in
    5.24        val pat_stricts = map pat_strict (pat_consts ~~ spec);
     6.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Jan 01 13:24:23 2014 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Jan 01 14:29:22 2014 +0100
     6.3 @@ -1523,7 +1523,7 @@
     6.4              (augment_sort thy1 pt_cp_sort
     6.5                (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
     6.6              (fn {context = ctxt, ...} => rtac rec_induct 1 THEN REPEAT
     6.7 -               (simp_tac (Simplifier.global_context thy11 HOL_basic_ss
     6.8 +               (simp_tac (put_simpset HOL_basic_ss ctxt
     6.9                    addsimps flat perm_simps'
    6.10                    addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
    6.11                  (resolve_tac rec_intrs THEN_ALL_NEW
    6.12 @@ -1925,9 +1925,9 @@
    6.13                        in
    6.14                          Goal.prove context'' [] []
    6.15                            (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
    6.16 -                          (fn _ => EVERY
    6.17 +                          (fn {context = ctxt, ...} => EVERY
    6.18                               [cut_facts_tac [th'] 1,
    6.19 -                              full_simp_tac (Simplifier.global_context thy11 HOL_ss  (* FIXME context'' (!?) *)
    6.20 +                              full_simp_tac (put_simpset HOL_ss ctxt
    6.21                                  addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
    6.22                                  addsimprocs [NominalPermeq.perm_simproc_app]) 1,
    6.23                                full_simp_tac (put_simpset HOL_ss context'' addsimps (calc_atm @
     7.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Jan 01 13:24:23 2014 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Jan 01 14:29:22 2014 +0100
     7.3 @@ -271,7 +271,7 @@
     7.4      val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
     7.5      val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
     7.6        ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
     7.7 -    val eqvt_ss = simpset_of (Simplifier.global_context thy HOL_basic_ss
     7.8 +    val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
     7.9        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    7.10        addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}],
    7.11          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
    7.12 @@ -452,13 +452,14 @@
    7.13                     concl))
    7.14            in map mk_prem prems end) cases_prems;
    7.15  
    7.16 -    val cases_eqvt_simpset = Simplifier.global_context thy HOL_ss
    7.17 +    val cases_eqvt_simpset = put_simpset HOL_ss (Proof_Context.init_global thy)
    7.18        addsimps eqvt_thms @ swap_simps @ perm_pi_simp
    7.19        addsimprocs [NominalPermeq.perm_simproc_app,
    7.20          NominalPermeq.perm_simproc_fun];
    7.21  
    7.22      val simp_fresh_atm = map
    7.23 -      (Simplifier.simplify (Simplifier.global_context thy HOL_basic_ss addsimps fresh_atm));
    7.24 +      (Simplifier.simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
    7.25 +        addsimps fresh_atm));
    7.26  
    7.27      fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt'))),
    7.28          prems') =
    7.29 @@ -608,7 +609,7 @@
    7.30           atoms)
    7.31        end;
    7.32      val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
    7.33 -    val eqvt_simpset = Simplifier.global_context thy HOL_basic_ss addsimps
    7.34 +    val eqvt_simpset = put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps
    7.35        (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
    7.36        [mk_perm_bool_simproc names,
    7.37         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     8.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Jan 01 13:24:23 2014 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Jan 01 14:29:22 2014 +0100
     8.3 @@ -290,7 +290,7 @@
     8.4      val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
     8.5      val pt2_atoms = map (fn a => Global_Theory.get_thm thy
     8.6        ("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
     8.7 -    val eqvt_ss = simpset_of (Simplifier.global_context thy HOL_basic_ss
     8.8 +    val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy)
     8.9        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    8.10        addsimprocs [mk_perm_bool_simproc ["Fun.id"],
    8.11          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]);
     9.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Wed Jan 01 13:24:23 2014 +0100
     9.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Wed Jan 01 14:29:22 2014 +0100
     9.3 @@ -66,12 +66,11 @@
     9.4      val distinct_goals = maps (massage_distinct o monomorphic_prop_of) distinct_thms;
     9.5      val refl_goal = HOLogic.mk_Trueprop (true_eq (Free ("x", fcT), Free ("x", fcT)));
     9.6  
     9.7 -    val simp_ctxt =
     9.8 -      Simplifier.global_context thy HOL_basic_ss
     9.9 -        addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms));
    9.10 -
    9.11      fun prove goal =
    9.12 -      Goal.prove_sorry_global thy [] [] goal (K (ALLGOALS (simp_tac simp_ctxt)))
    9.13 +      Goal.prove_sorry_global thy [] [] goal (fn {context = ctxt, ...} =>
    9.14 +        ALLGOALS (simp_tac
    9.15 +          (put_simpset HOL_basic_ss ctxt
    9.16 +            addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)))))
    9.17        |> Simpdata.mk_eq;
    9.18    in
    9.19      (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal)
    10.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Jan 01 13:24:23 2014 +0100
    10.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Jan 01 14:29:22 2014 +0100
    10.3 @@ -195,8 +195,8 @@
    10.4             EVERY [
    10.5              rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1,
    10.6              ALLGOALS (EVERY'
    10.7 -              [asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps case_rewrites),
    10.8 -               resolve_tac prems, asm_simp_tac (Simplifier.global_context thy HOL_basic_ss)])])
    10.9 +              [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites),
   10.10 +               resolve_tac prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])])
   10.11        |> Drule.export_without_context;
   10.12  
   10.13      val exh_name = Thm.derivation_name exhaust;
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Jan 01 13:24:23 2014 +0100
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Jan 01 14:29:22 2014 +0100
    11.3 @@ -185,12 +185,12 @@
    11.4    #> Conv.fconv_rule (nnf_conv ctxt)
    11.5    #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm ex_disj_distrib}])
    11.6  
    11.7 -fun rewrite_intros thy =
    11.8 -  Simplifier.full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [@{thm all_not_ex}])
    11.9 +fun rewrite_intros ctxt =
   11.10 +  Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm all_not_ex}])
   11.11    #> Simplifier.full_simplify
   11.12 -    (Simplifier.global_context thy HOL_basic_ss
   11.13 +    (put_simpset HOL_basic_ss ctxt
   11.14        addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
   11.15 -  #> split_conjuncts_in_assms (Proof_Context.init_global thy)
   11.16 +  #> split_conjuncts_in_assms ctxt
   11.17  
   11.18  fun print_specs options thy msg ths =
   11.19    if show_intermediate_results options then
   11.20 @@ -208,7 +208,7 @@
   11.21          if forall is_pred_equation specs then 
   11.22            map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs))
   11.23          else if forall (is_intro constname) specs then
   11.24 -          map (rewrite_intros thy) specs
   11.25 +          map (rewrite_intros ctxt) specs
   11.26          else
   11.27            error ("unexpected specification for constant " ^ quote constname ^ ":\n"
   11.28              ^ commas (map (quote o Display.string_of_thm_global thy) specs))
    12.1 --- a/src/HOL/Tools/TFL/rules.ML	Wed Jan 01 13:24:23 2014 +0100
    12.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed Jan 01 14:29:22 2014 +0100
    12.3 @@ -648,7 +648,7 @@
    12.4  
    12.5  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
    12.6   let val globals = func::G
    12.7 -     val ctxt0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
    12.8 +     val ctxt0 = empty_simpset (Proof_Context.init_global (Thm.theory_of_thm th))
    12.9       val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection];
   12.10       val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
   12.11       val cut_lemma' = cut_lemma RS eq_reflection
    13.1 --- a/src/HOL/Tools/TFL/tfl.ML	Wed Jan 01 13:24:23 2014 +0100
    13.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Jan 01 14:29:22 2014 +0100
    13.3 @@ -432,7 +432,7 @@
    13.4         not simplified. Otherwise large examples (Red-Black trees) are too
    13.5         slow.*)
    13.6       val case_simpset =
    13.7 -       Simplifier.global_context theory HOL_basic_ss
    13.8 +       put_simpset HOL_basic_ss (Proof_Context.init_global theory)
    13.9            addsimps case_rewrites
   13.10            |> fold (Simplifier.add_cong o #weak_case_cong o snd)
   13.11                (Symtab.dest (Datatype.get_all theory))
    14.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Jan 01 13:24:23 2014 +0100
    14.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Jan 01 14:29:22 2014 +0100
    14.3 @@ -406,8 +406,10 @@
    14.4  
    14.5  (**** preprocessor for code generator ****)
    14.6  
    14.7 -fun codegen_preproc thy =
    14.8 +(* FIXME unused!? *)
    14.9 +fun codegen_preproc thy =  (* FIXME proper context!? *)
   14.10    let
   14.11 +    val ctxt = Proof_Context.init_global thy;
   14.12      val {to_pred_simps, set_arities, pred_arities, ...} =
   14.13        Data.get (Context.Theory thy);
   14.14      fun preproc thm =
   14.15 @@ -417,7 +419,7 @@
   14.16              forall is_none xs) arities) (prop_of thm)
   14.17        then
   14.18          thm |>
   14.19 -        Simplifier.full_simplify (Simplifier.global_context thy HOL_basic_ss addsimprocs
   14.20 +        Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
   14.21            [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |>
   14.22          eta_contract_thm (is_pred pred_arities)
   14.23        else thm
    15.1 --- a/src/HOL/Tools/record.ML	Wed Jan 01 13:24:23 2014 +0100
    15.2 +++ b/src/HOL/Tools/record.ML	Wed Jan 01 14:29:22 2014 +0100
    15.3 @@ -1556,6 +1556,7 @@
    15.4        typ_thy
    15.5        |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd
    15.6        |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]);
    15.7 +    val defs_ctxt = Proof_Context.init_global defs_thy;
    15.8  
    15.9  
   15.10      (* prepare propositions *)
   15.11 @@ -1583,7 +1584,7 @@
   15.12        in Logic.mk_equals (Logic.all s (P $ s), fold_rev Logic.all vars_more (P $ ext)) end;
   15.13  
   15.14      val inject = timeit_msg ctxt "record extension inject proof:" (fn () =>
   15.15 -      simplify (Simplifier.global_context defs_thy HOL_ss)
   15.16 +      simplify (put_simpset HOL_ss defs_ctxt)
   15.17          (Goal.prove_sorry_global defs_thy [] [] inject_prop
   15.18            (fn {context = ctxt, ...} =>
   15.19              simp_tac (put_simpset HOL_basic_ss ctxt addsimps [ext_def]) 1 THEN
   15.20 @@ -1605,7 +1606,7 @@
   15.21          val cterm_ext = cterm_of defs_thy ext;
   15.22          val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE;
   15.23          val tactic1 =
   15.24 -          simp_tac (Simplifier.global_context defs_thy HOL_basic_ss addsimps [ext_def]) 1 THEN
   15.25 +          simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN
   15.26            REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1;
   15.27          val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1);
   15.28          val [halfway] = Seq.list_of (tactic1 start);
   15.29 @@ -1838,6 +1839,7 @@
   15.30        thy
   15.31        |> Sign.qualified_path false binding
   15.32        |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
   15.33 +    val ext_ctxt = Proof_Context.init_global ext_thy;
   15.34  
   15.35      val _ = timing_msg ctxt "record preparing definitions";
   15.36      val Type extension_scheme = extT;
   15.37 @@ -1935,7 +1937,7 @@
   15.38            val init_thm = named_cterm_instantiate insts updacc_eq_triv;
   15.39            val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1;
   15.40            val tactic =
   15.41 -            simp_tac (Simplifier.global_context ext_thy HOL_basic_ss addsimps ext_defs) 1 THEN
   15.42 +            simp_tac (put_simpset HOL_basic_ss ext_ctxt addsimps ext_defs) 1 THEN
   15.43              REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal);
   15.44            val updaccs = Seq.list_of (tactic init_thm);
   15.45          in
   15.46 @@ -2010,6 +2012,7 @@
   15.47                  map (rpair [Code.add_default_eqn_attribute]
   15.48                  o apfst (Binding.conceal o Binding.name))) (*FIXME Spec_Rules (?)*)
   15.49              [make_spec, fields_spec, extend_spec, truncate_spec]);
   15.50 +    val defs_ctxt = Proof_Context.init_global defs_thy;
   15.51  
   15.52      (* prepare propositions *)
   15.53      val _ = timing_msg ctxt "record preparing propositions";
   15.54 @@ -2078,7 +2081,7 @@
   15.55  
   15.56      val record_ss = get_simpset defs_thy;
   15.57      val sel_upd_ctxt =
   15.58 -      Simplifier.global_context defs_thy record_ss
   15.59 +      put_simpset record_ss defs_ctxt
   15.60          addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms);
   15.61  
   15.62      val (sel_convs, upd_convs) =
   15.63 @@ -2092,7 +2095,7 @@
   15.64      val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () =>
   15.65        let
   15.66          val symdefs = map Thm.symmetric (sel_defs @ upd_defs);
   15.67 -        val fold_ctxt = Simplifier.global_context defs_thy HOL_basic_ss addsimps symdefs;
   15.68 +        val fold_ctxt = put_simpset HOL_basic_ss defs_ctxt addsimps symdefs;
   15.69          val ua_congs = map (Drule.export_without_context o simplify fold_ctxt) upd_acc_cong_assists;
   15.70        in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end);
   15.71  
    16.1 --- a/src/Pure/raw_simplifier.ML	Wed Jan 01 13:24:23 2014 +0100
    16.2 +++ b/src/Pure/raw_simplifier.ML	Wed Jan 01 14:29:22 2014 +0100
    16.3 @@ -40,7 +40,6 @@
    16.4    val mk_simproc: string -> cterm list -> (Proof.context -> term -> thm option) -> simproc
    16.5    val simpset_of: Proof.context -> simpset
    16.6    val put_simpset: simpset -> Proof.context -> Proof.context
    16.7 -  val global_context: theory -> simpset -> Proof.context
    16.8    val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset
    16.9    val map_theory_simpset: (Proof.context -> Proof.context) -> theory -> theory
   16.10    val empty_simpset: Proof.context -> Proof.context
   16.11 @@ -388,8 +387,6 @@
   16.12      val Simpset ({bounds, depth, ...}, _) = context_ss;
   16.13    in Simpset (make_ss1 (rules, prems, bounds, depth), ss2) end);
   16.14  
   16.15 -fun global_context thy ss = Proof_Context.init_global thy |> put_simpset ss;
   16.16 -
   16.17  val empty_simpset = put_simpset empty_ss;
   16.18  
   16.19  fun map_theory_simpset f thy =
    17.1 --- a/src/Tools/Code/code_preproc.ML	Wed Jan 01 13:24:23 2014 +0100
    17.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Jan 01 14:29:22 2014 +0100
    17.3 @@ -143,7 +143,8 @@
    17.4      val resubst = curry (Term.betapplys o swap) all_vars;
    17.5    in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end;
    17.6  
    17.7 -fun lift_ss_conv f ss ct = f (Simplifier.global_context (theory_of_cterm ct) ss) ct;
    17.8 +fun lift_ss_conv f ss ct =  (* FIXME proper context!? *)
    17.9 +  f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss) ct;
   17.10  
   17.11  fun preprocess_conv thy =
   17.12    let
    18.1 --- a/src/Tools/Code/code_simp.ML	Wed Jan 01 13:24:23 2014 +0100
    18.2 +++ b/src/Tools/Code/code_simp.ML	Wed Jan 01 14:29:22 2014 +0100
    18.3 @@ -62,8 +62,8 @@
    18.4  fun simpset_program thy some_ss program =
    18.5    simpset_map (Proof_Context.init_global thy) (add_program program) (simpset_default thy some_ss);
    18.6  
    18.7 -fun lift_ss_conv f ss ct =
    18.8 -  f (Simplifier.global_context (theory_of_cterm ct) ss |> set_trace) ct;
    18.9 +fun lift_ss_conv f ss ct =  (* FIXME proper context!? *)
   18.10 +  f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss |> set_trace) ct;
   18.11  
   18.12  fun rewrite_modulo thy some_ss program =
   18.13    lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program);
    19.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Jan 01 13:24:23 2014 +0100
    19.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Jan 01 14:29:22 2014 +0100
    19.3 @@ -327,7 +327,7 @@
    19.4       (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
    19.5         If the premises get simplified, then the proofs could fail.*)
    19.6       val min_ss =
    19.7 -           (Simplifier.global_context thy empty_ss
    19.8 +           (empty_simpset (Proof_Context.init_global thy)
    19.9               |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)))
   19.10             setSolver (mk_solver "minimal"
   19.11                        (fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt)