# HG changeset patch # User wenzelm # Date 1388582962 -3600 # Node ID 51563048301064c9893e3eeadabc718bb4effad4 # Parent cb9d981fa9a0d074b4506c88361859107ae647fa clarified simplifier context; eliminated Simplifier.global_context; diff -r cb9d981fa9a0 -r 515630483010 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Jan 01 14:29:22 2014 +0100 @@ -227,12 +227,12 @@ 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} @@ -272,8 +272,8 @@ 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) = @@ -286,8 +286,8 @@ 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' @@ -317,16 +317,16 @@ 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 *) @@ -350,8 +350,8 @@ 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 @@ -362,8 +362,8 @@ 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' @@ -518,8 +518,8 @@ 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 @@ -586,12 +586,12 @@ 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 @@ -602,7 +602,7 @@ 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 @@ -617,13 +617,13 @@ 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 @@ -647,7 +647,7 @@ 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) @@ -656,7 +656,7 @@ 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 @@ -724,8 +724,8 @@ 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 @@ -738,13 +738,13 @@ 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 @@ -813,8 +813,8 @@ 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 @@ -832,8 +832,8 @@ 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 diff -r cb9d981fa9a0 -r 515630483010 src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Wed Jan 01 14:29:22 2014 +0100 @@ -71,9 +71,9 @@ val rules = [abs_inverse] @ con_betas @ @{thms take_con_rules} @ take_Suc_thms @ deflation_thms @ deflation_take_thms - val tac = simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1 + fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1 in - Goal.prove_global thy [] [] goal (K tac) + Goal.prove_global thy [] [] goal (tac o #context) end val take_apps = map prove_take_app con_specs in diff -r cb9d981fa9a0 -r 515630483010 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Jan 01 14:29:22 2014 +0100 @@ -158,7 +158,7 @@ fun prove_proj (lhs, rhs) = let fun tac ctxt = rewrite_goals_tac ctxt fixdef_thms THEN - (simp_tac (Simplifier.global_context thy beta_ss)) 1 + (simp_tac (put_simpset beta_ss ctxt)) 1 val goal = Logic.mk_equals (lhs, rhs) in Goal.prove_global thy [] [] goal (tac o #context) end val proj_thms = map prove_proj projs diff -r cb9d981fa9a0 -r 515630483010 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Wed Jan 01 14:29:22 2014 +0100 @@ -273,8 +273,8 @@ let val goal = mk_trp (mk_chain take_const) val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd} - val tac = simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1 - val thm = Goal.prove_global thy [] [] goal (K tac) + fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1 + val thm = Goal.prove_global thy [] [] goal (tac o #context) in add_qualified_simp_thm "chain_take" (dbind, thm) thy end @@ -287,8 +287,8 @@ val lhs = take_const $ @{term "0::nat"} val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT)) val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict} - val tac = simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps rules) 1 - val take_0_thm = Goal.prove_global thy [] [] goal (K tac) + fun tac ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) 1 + val take_0_thm = Goal.prove_global thy [] [] goal (tac o #context) in add_qualified_simp_thm "take_0" (dbind, take_0_thm) thy end @@ -307,8 +307,8 @@ val goal = mk_eqs (lhs, rhs) val simps = @{thms iterate_Suc fst_conv snd_conv} val rules = take_defs @ simps - val tac = simp_tac (Simplifier.global_context thy beta_ss addsimps rules) 1 - val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac) + fun tac ctxt = simp_tac (put_simpset beta_ss ctxt addsimps rules) 1 + val take_Suc_thm = Goal.prove_global thy [] [] goal (tac o #context) in add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy end @@ -330,11 +330,11 @@ @ deflation_abs_rep_thms @ get_deflation_thms thy in - Goal.prove_global thy [] [] goal (fn _ => + Goal.prove_global thy [] [] goal (fn {context = ctxt, ...} => EVERY [rtac @{thm nat.induct} 1, - simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps bottom_rules) 1, - asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps take_Suc_thms) 1, + simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1, + asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps take_Suc_thms) 1, REPEAT (etac @{thm conjE} 1 ORELSE resolve_tac deflation_rules 1 ORELSE atac 1)]) @@ -455,11 +455,11 @@ val rules1 = take_Suc_thms @ decisive_abs_rep_thms @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map} - val tac = EVERY [ + fun tac ctxt = EVERY [ rtac @{thm nat.induct} 1, - simp_tac (Simplifier.global_context thy HOL_ss addsimps rules0) 1, - asm_simp_tac (Simplifier.global_context thy HOL_ss addsimps rules1) 1] - in Goal.prove_global thy [] [] goal (K tac) end + simp_tac (put_simpset HOL_ss ctxt addsimps rules0) 1, + asm_simp_tac (put_simpset HOL_ss ctxt addsimps rules1) 1] + in Goal.prove_global thy [] [] goal (tac o #context) end fun conjuncts 1 thm = [thm] | conjuncts n thm = let val thmL = thm RS @{thm conjunct1} diff -r cb9d981fa9a0 -r 515630483010 src/HOL/HOLCF/ex/Pattern_Match.thy --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Wed Jan 01 14:29:22 2014 +0100 @@ -558,8 +558,8 @@ 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); @@ -573,8 +573,8 @@ 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); diff -r cb9d981fa9a0 -r 515630483010 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Jan 01 14:29:22 2014 +0100 @@ -1523,7 +1523,7 @@ (augment_sort thy1 pt_cp_sort (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps)))) (fn {context = ctxt, ...} => rtac rec_induct 1 THEN REPEAT - (simp_tac (Simplifier.global_context thy11 HOL_basic_ss + (simp_tac (put_simpset HOL_basic_ss ctxt addsimps flat perm_simps' addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN (resolve_tac rec_intrs THEN_ALL_NEW @@ -1925,9 +1925,9 @@ in Goal.prove context'' [] [] (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs')) - (fn _ => EVERY + (fn {context = ctxt, ...} => EVERY [cut_facts_tac [th'] 1, - full_simp_tac (Simplifier.global_context thy11 HOL_ss (* FIXME context'' (!?) *) + full_simp_tac (put_simpset HOL_ss ctxt addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap addsimprocs [NominalPermeq.perm_simproc_app]) 1, full_simp_tac (put_simpset HOL_ss context'' addsimps (calc_atm @ diff -r cb9d981fa9a0 -r 515630483010 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Wed Jan 01 14:29:22 2014 +0100 @@ -271,7 +271,7 @@ val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; val pt2_atoms = map (fn aT => Global_Theory.get_thm thy ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs; - val eqvt_ss = simpset_of (Simplifier.global_context thy HOL_basic_ss + val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc [@{const_name Fun.id}], NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]); @@ -452,13 +452,14 @@ concl)) in map mk_prem prems end) cases_prems; - val cases_eqvt_simpset = Simplifier.global_context thy HOL_ss + val cases_eqvt_simpset = put_simpset HOL_ss (Proof_Context.init_global thy) addsimps eqvt_thms @ swap_simps @ perm_pi_simp addsimprocs [NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; val simp_fresh_atm = map - (Simplifier.simplify (Simplifier.global_context thy HOL_basic_ss addsimps fresh_atm)); + (Simplifier.simplify (put_simpset HOL_basic_ss (Proof_Context.init_global thy) + addsimps fresh_atm)); fun mk_cases_proof ((((name, thss), elim), (prem, args, concl, (prems, ctxt'))), prems') = @@ -608,7 +609,7 @@ atoms) end; val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; - val eqvt_simpset = Simplifier.global_context thy HOL_basic_ss addsimps + val eqvt_simpset = put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs [mk_perm_bool_simproc names, NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]; diff -r cb9d981fa9a0 -r 515630483010 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Jan 01 14:29:22 2014 +0100 @@ -290,7 +290,7 @@ val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp"; val pt2_atoms = map (fn a => Global_Theory.get_thm thy ("pt_" ^ Long_Name.base_name a ^ "2")) atoms; - val eqvt_ss = simpset_of (Simplifier.global_context thy HOL_basic_ss + val eqvt_ss = simpset_of (put_simpset HOL_basic_ss (Proof_Context.init_global thy) addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc ["Fun.id"], NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun]); diff -r cb9d981fa9a0 -r 515630483010 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Wed Jan 01 14:29:22 2014 +0100 @@ -66,12 +66,11 @@ val distinct_goals = maps (massage_distinct o monomorphic_prop_of) distinct_thms; val refl_goal = HOLogic.mk_Trueprop (true_eq (Free ("x", fcT), Free ("x", fcT))); - val simp_ctxt = - Simplifier.global_context thy HOL_basic_ss - addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms)); - fun prove goal = - Goal.prove_sorry_global thy [] [] goal (K (ALLGOALS (simp_tac simp_ctxt))) + Goal.prove_sorry_global thy [] [] goal (fn {context = ctxt, ...} => + ALLGOALS (simp_tac + (put_simpset HOL_basic_ss ctxt + addsimps (map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms))))) |> Simpdata.mk_eq; in (map prove (triv_inject_goals @ inject_goals @ distinct_goals), prove refl_goal) diff -r cb9d981fa9a0 -r 515630483010 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Jan 01 14:29:22 2014 +0100 @@ -195,8 +195,8 @@ EVERY [ rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1, ALLGOALS (EVERY' - [asm_simp_tac (Simplifier.global_context thy HOL_basic_ss addsimps case_rewrites), - resolve_tac prems, asm_simp_tac (Simplifier.global_context thy HOL_basic_ss)])]) + [asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps case_rewrites), + resolve_tac prems, asm_simp_tac (put_simpset HOL_basic_ss ctxt)])]) |> Drule.export_without_context; val exh_name = Thm.derivation_name exhaust; diff -r cb9d981fa9a0 -r 515630483010 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Wed Jan 01 14:29:22 2014 +0100 @@ -185,12 +185,12 @@ #> Conv.fconv_rule (nnf_conv ctxt) #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm ex_disj_distrib}]) -fun rewrite_intros thy = - Simplifier.full_simplify (Simplifier.global_context thy HOL_basic_ss addsimps [@{thm all_not_ex}]) +fun rewrite_intros ctxt = + Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm all_not_ex}]) #> Simplifier.full_simplify - (Simplifier.global_context thy HOL_basic_ss + (put_simpset HOL_basic_ss ctxt addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps}) - #> split_conjuncts_in_assms (Proof_Context.init_global thy) + #> split_conjuncts_in_assms ctxt fun print_specs options thy msg ths = if show_intermediate_results options then @@ -208,7 +208,7 @@ if forall is_pred_equation specs then map (split_conjuncts_in_assms ctxt) (introrulify thy (map (rewrite ctxt) specs)) else if forall (is_intro constname) specs then - map (rewrite_intros thy) specs + map (rewrite_intros ctxt) specs else error ("unexpected specification for constant " ^ quote constname ^ ":\n" ^ commas (map (quote o Display.string_of_thm_global thy) specs)) diff -r cb9d981fa9a0 -r 515630483010 src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/Tools/TFL/rules.ML Wed Jan 01 14:29:22 2014 +0100 @@ -648,7 +648,7 @@ fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th = let val globals = func::G - val ctxt0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss + val ctxt0 = empty_simpset (Proof_Context.init_global (Thm.theory_of_thm th)) val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection]; val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref val cut_lemma' = cut_lemma RS eq_reflection diff -r cb9d981fa9a0 -r 515630483010 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Wed Jan 01 14:29:22 2014 +0100 @@ -432,7 +432,7 @@ not simplified. Otherwise large examples (Red-Black trees) are too slow.*) val case_simpset = - Simplifier.global_context theory HOL_basic_ss + put_simpset HOL_basic_ss (Proof_Context.init_global theory) addsimps case_rewrites |> fold (Simplifier.add_cong o #weak_case_cong o snd) (Symtab.dest (Datatype.get_all theory)) diff -r cb9d981fa9a0 -r 515630483010 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/Tools/inductive_set.ML Wed Jan 01 14:29:22 2014 +0100 @@ -406,8 +406,10 @@ (**** preprocessor for code generator ****) -fun codegen_preproc thy = +(* FIXME unused!? *) +fun codegen_preproc thy = (* FIXME proper context!? *) let + val ctxt = Proof_Context.init_global thy; val {to_pred_simps, set_arities, pred_arities, ...} = Data.get (Context.Theory thy); fun preproc thm = @@ -417,7 +419,7 @@ forall is_none xs) arities) (prop_of thm) then thm |> - Simplifier.full_simplify (Simplifier.global_context thy HOL_basic_ss addsimprocs + Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs [to_pred_simproc (mem_Collect_eq :: @{thm split_conv} :: to_pred_simps)]) |> eta_contract_thm (is_pred pred_arities) else thm diff -r cb9d981fa9a0 -r 515630483010 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/HOL/Tools/record.ML Wed Jan 01 14:29:22 2014 +0100 @@ -1556,6 +1556,7 @@ typ_thy |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]); + val defs_ctxt = Proof_Context.init_global defs_thy; (* prepare propositions *) @@ -1583,7 +1584,7 @@ in Logic.mk_equals (Logic.all s (P $ s), fold_rev Logic.all vars_more (P $ ext)) end; val inject = timeit_msg ctxt "record extension inject proof:" (fn () => - simplify (Simplifier.global_context defs_thy HOL_ss) + simplify (put_simpset HOL_ss defs_ctxt) (Goal.prove_sorry_global defs_thy [] [] inject_prop (fn {context = ctxt, ...} => simp_tac (put_simpset HOL_basic_ss ctxt addsimps [ext_def]) 1 THEN @@ -1605,7 +1606,7 @@ val cterm_ext = cterm_of defs_thy ext; val start = named_cterm_instantiate [("y", cterm_ext)] surject_assist_idE; val tactic1 = - simp_tac (Simplifier.global_context defs_thy HOL_basic_ss addsimps [ext_def]) 1 THEN + simp_tac (put_simpset HOL_basic_ss defs_ctxt addsimps [ext_def]) 1 THEN REPEAT_ALL_NEW Iso_Tuple_Support.iso_tuple_intros_tac 1; val tactic2 = REPEAT (rtac surject_assistI 1 THEN rtac refl 1); val [halfway] = Seq.list_of (tactic1 start); @@ -1838,6 +1839,7 @@ thy |> Sign.qualified_path false binding |> extension_definition extension_name fields alphas_ext zeta moreT more vars; + val ext_ctxt = Proof_Context.init_global ext_thy; val _ = timing_msg ctxt "record preparing definitions"; val Type extension_scheme = extT; @@ -1935,7 +1937,7 @@ val init_thm = named_cterm_instantiate insts updacc_eq_triv; val terminal = rtac updacc_eq_idI 1 THEN rtac refl 1; val tactic = - simp_tac (Simplifier.global_context ext_thy HOL_basic_ss addsimps ext_defs) 1 THEN + simp_tac (put_simpset HOL_basic_ss ext_ctxt addsimps ext_defs) 1 THEN REPEAT (Iso_Tuple_Support.iso_tuple_intros_tac 1 ORELSE terminal); val updaccs = Seq.list_of (tactic init_thm); in @@ -2010,6 +2012,7 @@ map (rpair [Code.add_default_eqn_attribute] o apfst (Binding.conceal o Binding.name))) (*FIXME Spec_Rules (?)*) [make_spec, fields_spec, extend_spec, truncate_spec]); + val defs_ctxt = Proof_Context.init_global defs_thy; (* prepare propositions *) val _ = timing_msg ctxt "record preparing propositions"; @@ -2078,7 +2081,7 @@ val record_ss = get_simpset defs_thy; val sel_upd_ctxt = - Simplifier.global_context defs_thy record_ss + put_simpset record_ss defs_ctxt addsimps (sel_defs @ accessor_thms @ upd_defs @ updator_thms); val (sel_convs, upd_convs) = @@ -2092,7 +2095,7 @@ val (fold_congs, unfold_congs) = timeit_msg ctxt "record upd fold/unfold congs:" (fn () => let val symdefs = map Thm.symmetric (sel_defs @ upd_defs); - val fold_ctxt = Simplifier.global_context defs_thy HOL_basic_ss addsimps symdefs; + val fold_ctxt = put_simpset HOL_basic_ss defs_ctxt addsimps symdefs; val ua_congs = map (Drule.export_without_context o simplify fold_ctxt) upd_acc_cong_assists; in (ua_congs RL [updacc_foldE], ua_congs RL [updacc_unfoldE]) end); diff -r cb9d981fa9a0 -r 515630483010 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/Pure/raw_simplifier.ML Wed Jan 01 14:29:22 2014 +0100 @@ -40,7 +40,6 @@ val mk_simproc: string -> cterm list -> (Proof.context -> term -> thm option) -> simproc val simpset_of: Proof.context -> simpset val put_simpset: simpset -> Proof.context -> Proof.context - val global_context: theory -> simpset -> Proof.context val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset val map_theory_simpset: (Proof.context -> Proof.context) -> theory -> theory val empty_simpset: Proof.context -> Proof.context @@ -388,8 +387,6 @@ val Simpset ({bounds, depth, ...}, _) = context_ss; in Simpset (make_ss1 (rules, prems, bounds, depth), ss2) end); -fun global_context thy ss = Proof_Context.init_global thy |> put_simpset ss; - val empty_simpset = put_simpset empty_ss; fun map_theory_simpset f thy = diff -r cb9d981fa9a0 -r 515630483010 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/Tools/Code/code_preproc.ML Wed Jan 01 14:29:22 2014 +0100 @@ -143,7 +143,8 @@ val resubst = curry (Term.betapplys o swap) all_vars; in (resubst, term_of_conv thy conv (fold_rev lambda all_vars t)) end; -fun lift_ss_conv f ss ct = f (Simplifier.global_context (theory_of_cterm ct) ss) ct; +fun lift_ss_conv f ss ct = (* FIXME proper context!? *) + f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss) ct; fun preprocess_conv thy = let diff -r cb9d981fa9a0 -r 515630483010 src/Tools/Code/code_simp.ML --- a/src/Tools/Code/code_simp.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/Tools/Code/code_simp.ML Wed Jan 01 14:29:22 2014 +0100 @@ -62,8 +62,8 @@ fun simpset_program thy some_ss program = simpset_map (Proof_Context.init_global thy) (add_program program) (simpset_default thy some_ss); -fun lift_ss_conv f ss ct = - f (Simplifier.global_context (theory_of_cterm ct) ss |> set_trace) ct; +fun lift_ss_conv f ss ct = (* FIXME proper context!? *) + f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss |> set_trace) ct; fun rewrite_modulo thy some_ss program = lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program); diff -r cb9d981fa9a0 -r 515630483010 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Wed Jan 01 13:24:23 2014 +0100 +++ b/src/ZF/Tools/inductive_package.ML Wed Jan 01 14:29:22 2014 +0100 @@ -327,7 +327,7 @@ (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules. If the premises get simplified, then the proofs could fail.*) val min_ss = - (Simplifier.global_context thy empty_ss + (empty_simpset (Proof_Context.init_global thy) |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))) setSolver (mk_solver "minimal" (fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt)