renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
authorwenzelm
Fri Feb 19 16:11:45 2010 +0100 (2010-02-19)
changeset 35232f588e1169c8b
parent 35231 98e52f522357
child 35233 6af1caf7be69
renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
src/FOL/simpdata.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Prolog/prolog.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/record.ML
src/HOL/Tools/simpdata.ML
src/Provers/hypsubst.ML
src/Pure/codegen.ML
src/Pure/meta_simplifier.ML
src/Pure/simplifier.ML
src/Sequents/simpdata.ML
src/Tools/Code/code_preproc.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/FOL/simpdata.ML	Fri Feb 19 11:56:11 2010 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Fri Feb 19 16:11:45 2010 +0100
     1.3 @@ -128,7 +128,7 @@
     1.4  
     1.5  (*No simprules, but basic infastructure for simplification*)
     1.6  val FOL_basic_ss =
     1.7 -  Simplifier.theory_context @{theory} empty_ss
     1.8 +  Simplifier.global_context @{theory} empty_ss
     1.9    setsubgoaler asm_simp_tac
    1.10    setSSolver (mk_solver "FOL safe" safe_solver)
    1.11    setSolver (mk_solver "FOL unsafe" unsafe_solver)
     2.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Feb 19 11:56:11 2010 +0100
     2.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Fri Feb 19 16:11:45 2010 +0100
     2.3 @@ -82,12 +82,12 @@
     2.4      (* Transform the term*)
     2.5      val (t,np,nh) = prepare_for_linr thy q g
     2.6      (* Some simpsets for dealing with mod div abs and nat*)
     2.7 -    val simpset0 = Simplifier.theory_context thy HOL_basic_ss addsimps comp_arith
     2.8 +    val simpset0 = Simplifier.global_context thy HOL_basic_ss addsimps comp_arith
     2.9      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
    2.10      (* Theorem for the nat --> int transformation *)
    2.11     val pre_thm = Seq.hd (EVERY
    2.12        [simp_tac simpset0 1,
    2.13 -       TRY (simp_tac (Simplifier.theory_context thy ferrack_ss) 1)]
    2.14 +       TRY (simp_tac (Simplifier.global_context thy ferrack_ss) 1)]
    2.15        (trivial ct))
    2.16      fun assm_tac i = REPEAT_DETERM_N nh (assume_tac i)
    2.17      (* The result of the quantifier elimination *)
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Feb 19 11:56:11 2010 +0100
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Feb 19 16:11:45 2010 +0100
     3.3 @@ -1248,7 +1248,7 @@
     3.4  fun rewrite_hol4_term t thy =
     3.5      let
     3.6          val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
     3.7 -        val hol4ss = Simplifier.theory_context thy empty_ss
     3.8 +        val hol4ss = Simplifier.global_context thy empty_ss
     3.9            setmksimps single addsimps hol4rews1
    3.10      in
    3.11          Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
     4.1 --- a/src/HOL/Import/shuffler.ML	Fri Feb 19 11:56:11 2010 +0100
     4.2 +++ b/src/HOL/Import/shuffler.ML	Fri Feb 19 16:11:45 2010 +0100
     4.3 @@ -488,7 +488,7 @@
     4.4  fun norm_term thy t =
     4.5      let
     4.6          val norms = ShuffleData.get thy
     4.7 -        val ss = Simplifier.theory_context thy empty_ss
     4.8 +        val ss = Simplifier.global_context thy empty_ss
     4.9            setmksimps single
    4.10            addsimps (map (Thm.transfer thy) norms)
    4.11            addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
     5.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Feb 19 11:56:11 2010 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Feb 19 16:11:45 2010 +0100
     5.3 @@ -1547,7 +1547,7 @@
     5.4              (augment_sort thy1 pt_cp_sort
     5.5                (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps))))
     5.6              (fn _ => rtac rec_induct 1 THEN REPEAT
     5.7 -               (simp_tac (Simplifier.theory_context thy11 HOL_basic_ss
     5.8 +               (simp_tac (Simplifier.global_context thy11 HOL_basic_ss
     5.9                    addsimps flat perm_simps'
    5.10                    addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN
    5.11                  (resolve_tac rec_intrs THEN_ALL_NEW
    5.12 @@ -1951,7 +1951,7 @@
    5.13                            (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs'))
    5.14                            (fn _ => EVERY
    5.15                               [cut_facts_tac [th'] 1,
    5.16 -                              full_simp_tac (Simplifier.theory_context thy11 HOL_ss
    5.17 +                              full_simp_tac (Simplifier.global_context thy11 HOL_ss
    5.18                                  addsimps rec_eqns @ pi1_pi2_eqs @ perm_swap
    5.19                                  addsimprocs [NominalPermeq.perm_simproc_app]) 1,
    5.20                                full_simp_tac (HOL_ss addsimps (calc_atm @
     6.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Feb 19 11:56:11 2010 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Feb 19 16:11:45 2010 +0100
     6.3 @@ -274,7 +274,7 @@
     6.4      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
     6.5      val pt2_atoms = map (fn aT => PureThy.get_thm thy
     6.6        ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
     6.7 -    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
     6.8 +    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
     6.9        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    6.10        addsimprocs [mk_perm_bool_simproc ["Fun.id"],
    6.11          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
    6.12 @@ -455,7 +455,7 @@
    6.13                     concl))
    6.14            in map mk_prem prems end) cases_prems;
    6.15  
    6.16 -    val cases_eqvt_ss = Simplifier.theory_context thy HOL_ss
    6.17 +    val cases_eqvt_ss = Simplifier.global_context thy HOL_ss
    6.18        addsimps eqvt_thms @ swap_simps @ perm_pi_simp
    6.19        addsimprocs [NominalPermeq.perm_simproc_app,
    6.20          NominalPermeq.perm_simproc_fun];
    6.21 @@ -611,7 +611,7 @@
    6.22           atoms)
    6.23        end;
    6.24      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    6.25 -    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss addsimps
    6.26 +    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
    6.27        (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
    6.28        [mk_perm_bool_simproc names,
    6.29         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     7.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Feb 19 11:56:11 2010 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Feb 19 16:11:45 2010 +0100
     7.3 @@ -292,7 +292,7 @@
     7.4      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
     7.5      val pt2_atoms = map (fn a => PureThy.get_thm thy
     7.6        ("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
     7.7 -    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
     7.8 +    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
     7.9        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    7.10        addsimprocs [mk_perm_bool_simproc ["Fun.id"],
    7.11          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     8.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Fri Feb 19 11:56:11 2010 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Feb 19 16:11:45 2010 +0100
     8.3 @@ -143,7 +143,7 @@
     8.4  fun perm_simp_gen stac dyn_thms eqvt_thms ss i = 
     8.5      ("general simplification of permutations", fn st =>
     8.6      let
     8.7 -       val ss' = Simplifier.theory_context (theory_of_thm st) ss
     8.8 +       val ss' = Simplifier.global_context (theory_of_thm st) ss
     8.9           addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
    8.10           delcongs weak_congs
    8.11           addcongs strong_congs
    8.12 @@ -221,7 +221,7 @@
    8.13    ("analysing permutation compositions on the lhs",
    8.14     fn st => EVERY
    8.15       [rtac trans i,
    8.16 -      asm_full_simp_tac (Simplifier.theory_context (theory_of_thm st) empty_ss
    8.17 +      asm_full_simp_tac (Simplifier.global_context (theory_of_thm st) empty_ss
    8.18          addsimprocs [perm_compose_simproc]) i,
    8.19        asm_full_simp_tac (HOL_basic_ss addsimps [perm_aux_fold]) i] st);
    8.20  
     9.1 --- a/src/HOL/Prolog/prolog.ML	Fri Feb 19 11:56:11 2010 +0100
     9.2 +++ b/src/HOL/Prolog/prolog.ML	Fri Feb 19 16:11:45 2010 +0100
     9.3 @@ -59,7 +59,7 @@
     9.4  in map zero_var_indexes (at thm) end;
     9.5  
     9.6  val atomize_ss =
     9.7 -  Simplifier.theory_context @{theory} empty_ss
     9.8 +  Simplifier.global_context @{theory} empty_ss
     9.9    setmksimps (mksimps mksimps_pairs)
    9.10    addsimps [
    9.11          all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    10.1 --- a/src/HOL/Tools/TFL/rules.ML	Fri Feb 19 11:56:11 2010 +0100
    10.2 +++ b/src/HOL/Tools/TFL/rules.ML	Fri Feb 19 16:11:45 2010 +0100
    10.3 @@ -663,7 +663,7 @@
    10.4  
    10.5  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
    10.6   let val globals = func::G
    10.7 -     val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss
    10.8 +     val ss0 = Simplifier.global_context (Thm.theory_of_thm th) empty_ss
    10.9       val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
   10.10       val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
   10.11       val dummy = term_ref := []
    11.1 --- a/src/HOL/Tools/TFL/tfl.ML	Fri Feb 19 11:56:11 2010 +0100
    11.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Fri Feb 19 16:11:45 2010 +0100
    11.3 @@ -440,7 +440,7 @@
    11.4       (*case_ss causes minimal simplification: bodies of case expressions are
    11.5         not simplified. Otherwise large examples (Red-Black trees) are too
    11.6         slow.*)
    11.7 -     val case_ss = Simplifier.theory_context theory
    11.8 +     val case_ss = Simplifier.global_context theory
    11.9         (HOL_basic_ss addcongs
   11.10           (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites)
   11.11       val corollaries' = map (Simplifier.simplify case_ss) corollaries
    12.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Feb 19 11:56:11 2010 +0100
    12.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Feb 19 16:11:45 2010 +0100
    12.3 @@ -859,7 +859,7 @@
    12.4      addsimps [@{thm imp_conv_disj}, @{thm iff_conv_conj_imp}, @{thm de_Morgan_disj},
    12.5        @{thm de_Morgan_conj}, @{thm not_all}, @{thm not_ex}, @{thm not_not}];
    12.6    fun prem_nnf_tac i st =
    12.7 -    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
    12.8 +    full_simp_tac (Simplifier.global_context (Thm.theory_of_thm st) nnf_simpset) i st;
    12.9  in
   12.10  fun refute_tac test prep_tac ref_tac =
   12.11    let val refute_prems_tac =
    13.1 --- a/src/HOL/Tools/record.ML	Fri Feb 19 11:56:11 2010 +0100
    13.2 +++ b/src/HOL/Tools/record.ML	Fri Feb 19 16:11:45 2010 +0100
    13.3 @@ -518,7 +518,7 @@
    13.4  
    13.5  val is_selector = Symtab.defined o #selectors o get_sel_upd;
    13.6  val get_updates = Symtab.lookup o #updates o get_sel_upd;
    13.7 -fun get_ss_with_context getss thy = Simplifier.theory_context thy (getss (get_sel_upd thy));
    13.8 +fun get_ss_with_context getss thy = Simplifier.global_context thy (getss (get_sel_upd thy));
    13.9  
   13.10  val get_simpset = get_ss_with_context #simpset;
   13.11  val get_sel_upd_defs = get_ss_with_context #defset;
    14.1 --- a/src/HOL/Tools/simpdata.ML	Fri Feb 19 11:56:11 2010 +0100
    14.2 +++ b/src/HOL/Tools/simpdata.ML	Fri Feb 19 16:11:45 2010 +0100
    14.3 @@ -164,7 +164,7 @@
    14.4     ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
    14.5  
    14.6  val HOL_basic_ss =
    14.7 -  Simplifier.theory_context @{theory} empty_ss
    14.8 +  Simplifier.global_context @{theory} empty_ss
    14.9      setsubgoaler asm_simp_tac
   14.10      setSSolver safe_solver
   14.11      setSolver unsafe_solver
    15.1 --- a/src/Provers/hypsubst.ML	Fri Feb 19 11:56:11 2010 +0100
    15.2 +++ b/src/Provers/hypsubst.ML	Fri Feb 19 16:11:45 2010 +0100
    15.3 @@ -156,7 +156,7 @@
    15.4      let fun tac i st = SUBGOAL (fn (Bi, _) =>
    15.5        let
    15.6          val (k, _) = eq_var bnd true Bi
    15.7 -        val hyp_subst_ss = Simplifier.theory_context (Thm.theory_of_thm st) empty_ss
    15.8 +        val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
    15.9            setmksimps (mk_eqs bnd)
   15.10        in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
   15.11          etac thin_rl i, rotate_tac (~k) i]
    16.1 --- a/src/Pure/codegen.ML	Fri Feb 19 11:56:11 2010 +0100
    16.2 +++ b/src/Pure/codegen.ML	Fri Feb 19 16:11:45 2010 +0100
    16.3 @@ -299,7 +299,7 @@
    16.4  val del_unfold = map_unfold o MetaSimplifier.del_simp;
    16.5  
    16.6  fun unfold_preprocessor thy =
    16.7 -  let val ss = Simplifier.theory_context thy (UnfoldData.get thy)
    16.8 +  let val ss = Simplifier.global_context thy (UnfoldData.get thy)
    16.9    in map (Thm.transfer thy #> Simplifier.full_simplify ss) end;
   16.10  
   16.11  
    17.1 --- a/src/Pure/meta_simplifier.ML	Fri Feb 19 11:56:11 2010 +0100
    17.2 +++ b/src/Pure/meta_simplifier.ML	Fri Feb 19 16:11:45 2010 +0100
    17.3 @@ -111,7 +111,7 @@
    17.4    val inherit_context: simpset -> simpset -> simpset
    17.5    val the_context: simpset -> Proof.context
    17.6    val context: Proof.context -> simpset -> simpset
    17.7 -  val theory_context: theory  -> simpset -> simpset
    17.8 +  val global_context: theory  -> simpset -> simpset
    17.9    val debug_bounds: bool Unsynchronized.ref
   17.10    val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
   17.11    val set_solvers: solver list -> simpset -> simpset
   17.12 @@ -341,7 +341,7 @@
   17.13  fun context ctxt =
   17.14    map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
   17.15  
   17.16 -val theory_context = context o ProofContext.init;
   17.17 +val global_context = context o ProofContext.init;
   17.18  
   17.19  fun activate_context thy ss =
   17.20    let
   17.21 @@ -1241,7 +1241,7 @@
   17.22  
   17.23  fun rewrite _ [] ct = Thm.reflexive ct
   17.24    | rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
   17.25 -      (theory_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
   17.26 +      (global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
   17.27  
   17.28  fun simplify full thms = Conv.fconv_rule (rewrite full thms);
   17.29  val rewrite_rule = simplify true;
   17.30 @@ -1255,7 +1255,7 @@
   17.31  (*Rewrite the subgoals of a proof state (represented by a theorem)*)
   17.32  fun rewrite_goals_rule thms th =
   17.33    Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
   17.34 -    (theory_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
   17.35 +    (global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
   17.36  
   17.37  (*Rewrite the subgoal of a proof state (represented by a theorem)*)
   17.38  fun rewrite_goal_rule mode prover ss i thm =
   17.39 @@ -1279,7 +1279,7 @@
   17.40  fun rewrite_goal_tac rews =
   17.41    let val ss = empty_ss addsimps rews in
   17.42      fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
   17.43 -      (theory_context (Thm.theory_of_thm st) ss) i st
   17.44 +      (global_context (Thm.theory_of_thm st) ss) i st
   17.45    end;
   17.46  
   17.47  (*Prunes all redundant parameters from the proof state by rewriting.
   17.48 @@ -1317,7 +1317,7 @@
   17.49  fun gen_norm_hhf ss th =
   17.50    (if Drule.is_norm_hhf (Thm.prop_of th) then th
   17.51     else Conv.fconv_rule
   17.52 -    (rewrite_cterm (true, false, false) (K (K NONE)) (theory_context (Thm.theory_of_thm th) ss)) th)
   17.53 +    (rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th)
   17.54    |> Thm.adjust_maxidx_thm ~1
   17.55    |> Drule.gen_all;
   17.56  
    18.1 --- a/src/Pure/simplifier.ML	Fri Feb 19 11:56:11 2010 +0100
    18.2 +++ b/src/Pure/simplifier.ML	Fri Feb 19 16:11:45 2010 +0100
    18.3 @@ -36,7 +36,7 @@
    18.4    val inherit_context: simpset -> simpset -> simpset
    18.5    val the_context: simpset -> Proof.context
    18.6    val context: Proof.context -> simpset -> simpset
    18.7 -  val theory_context: theory  -> simpset -> simpset
    18.8 +  val global_context: theory  -> simpset -> simpset
    18.9    val simproc_i: theory -> string -> term list
   18.10      -> (theory -> simpset -> term -> thm option) -> simproc
   18.11    val simproc: theory -> string -> string list
    19.1 --- a/src/Sequents/simpdata.ML	Fri Feb 19 11:56:11 2010 +0100
    19.2 +++ b/src/Sequents/simpdata.ML	Fri Feb 19 16:11:45 2010 +0100
    19.3 @@ -68,7 +68,7 @@
    19.4  
    19.5  (*No simprules, but basic infrastructure for simplification*)
    19.6  val LK_basic_ss =
    19.7 -  Simplifier.theory_context @{theory} empty_ss
    19.8 +  Simplifier.global_context @{theory} empty_ss
    19.9      setsubgoaler asm_simp_tac
   19.10      setSSolver (mk_solver "safe" safe_solver)
   19.11      setSolver (mk_solver "unsafe" unsafe_solver)
    20.1 --- a/src/Tools/Code/code_preproc.ML	Fri Feb 19 11:56:11 2010 +0100
    20.2 +++ b/src/Tools/Code/code_preproc.ML	Fri Feb 19 16:11:45 2010 +0100
    20.3 @@ -129,7 +129,7 @@
    20.4  
    20.5  fun preprocess thy =
    20.6    let
    20.7 -    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
    20.8 +    val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
    20.9    in
   20.10      preprocess_functrans thy
   20.11      #> (map o apfst) (rewrite_eqn pre)
   20.12 @@ -137,7 +137,7 @@
   20.13  
   20.14  fun preprocess_conv thy ct =
   20.15    let
   20.16 -    val pre = (Simplifier.theory_context thy o #pre o the_thmproc) thy;
   20.17 +    val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   20.18    in
   20.19      ct
   20.20      |> Simplifier.rewrite pre
   20.21 @@ -146,7 +146,7 @@
   20.22  
   20.23  fun postprocess_conv thy ct =
   20.24    let
   20.25 -    val post = (Simplifier.theory_context thy o #post o the_thmproc) thy;
   20.26 +    val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
   20.27    in
   20.28      ct
   20.29      |> AxClass.overload_conv thy
    21.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Feb 19 11:56:11 2010 +0100
    21.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Feb 19 16:11:45 2010 +0100
    21.3 @@ -327,7 +327,7 @@
    21.4  
    21.5       (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
    21.6         If the premises get simplified, then the proofs could fail.*)
    21.7 -     val min_ss = Simplifier.theory_context thy empty_ss
    21.8 +     val min_ss = Simplifier.global_context thy empty_ss
    21.9             setmksimps (map mk_eq o ZF_atomize o gen_all)
   21.10             setSolver (mk_solver "minimal"
   21.11                        (fn prems => resolve_tac (triv_rls@prems)