src/HOL/HOL.thy
 changeset 51717 9e7d1c139569 parent 51692 ecd34f863242 child 51798 ad3a241def73
```     1.1 --- a/src/HOL/HOL.thy	Tue Apr 16 17:54:14 2013 +0200
1.2 +++ b/src/HOL/HOL.thy	Thu Apr 18 17:07:01 2013 +0200
1.3 @@ -1189,7 +1189,7 @@
1.4  ML_file "Tools/simpdata.ML"
1.5  ML {* open Simpdata *}
1.6
1.7 -setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *}
1.8 +setup {* map_theory_simpset (put_simpset HOL_basic_ss) *}
1.9
1.10  simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
1.11  simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
1.12 @@ -1241,10 +1241,9 @@
1.13     case t
1.14      of Abs (_, _, t') => count_loose t' 0 <= 1
1.15       | _ => true;
1.16 -in fn _ => fn ss => fn ct => if is_trivial_let (Thm.term_of ct)
1.17 +in fn _ => fn ctxt => fn ct => if is_trivial_let (Thm.term_of ct)
1.18    then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
1.19    else let (*Norbert Schirmer's case*)
1.20 -    val ctxt = Simplifier.the_context ss;
1.21      val thy = Proof_Context.theory_of ctxt;
1.22      val t = Thm.term_of ct;
1.23      val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
1.24 @@ -1258,7 +1257,7 @@
1.25            val cx = cterm_of thy x;
1.26            val {T = xT, ...} = rep_cterm cx;
1.27            val cf = cterm_of thy f;
1.28 -          val fx_g = Simplifier.rewrite ss (Thm.apply cf cx);
1.29 +          val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
1.30            val (_ \$ _ \$ g) = prop_of fx_g;
1.31            val g' = abstract_over (x,g);
1.32            val abs_g'= Abs (n,xT,g');
1.33 @@ -1345,7 +1344,7 @@
1.34  lemmas [cong] = imp_cong simp_implies_cong
1.35  lemmas [split] = split_if
1.36
1.37 -ML {* val HOL_ss = @{simpset} *}
1.38 +ML {* val HOL_ss = simpset_of @{context} *}
1.39
1.40  text {* Simplifies x assuming c and y assuming ~c *}
1.41  lemma if_cong:
1.42 @@ -1482,13 +1481,13 @@
1.43      addsimprocs
1.44        [Simplifier.simproc_global @{theory} "swap_induct_false"
1.45           ["induct_false ==> PROP P ==> PROP Q"]
1.46 -         (fn _ => fn _ =>
1.47 +         (fn _ =>
1.48              (fn _ \$ (P as _ \$ @{const induct_false}) \$ (_ \$ Q \$ _) =>
1.49                    if P <> Q then SOME Drule.swap_prems_eq else NONE
1.50                | _ => NONE)),
1.51         Simplifier.simproc_global @{theory} "induct_equal_conj_curry"
1.52           ["induct_conj P Q ==> PROP R"]
1.53 -         (fn _ => fn _ =>
1.54 +         (fn _ =>
1.55              (fn _ \$ (_ \$ P) \$ _ =>
1.56                  let
1.57                    fun is_conj (@{const induct_conj} \$ P \$ Q) =
1.58 @@ -1583,7 +1582,7 @@
1.59  signature REORIENT_PROC =
1.60  sig
1.61    val add : (term -> bool) -> theory -> theory
1.62 -  val proc : morphism -> simpset -> cterm -> thm option
1.63 +  val proc : morphism -> Proof.context -> cterm -> thm option
1.64  end;
1.65
1.66  structure Reorient_Proc : REORIENT_PROC =
1.67 @@ -1599,9 +1598,8 @@
1.68    fun matches thy t = exists (fn (m, _) => m t) (Data.get thy);
1.69
1.70    val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
1.71 -  fun proc phi ss ct =
1.72 +  fun proc phi ctxt ct =
1.73      let
1.74 -      val ctxt = Simplifier.the_context ss;
1.75        val thy = Proof_Context.theory_of ctxt;
1.76      in
1.77        case Thm.term_of ct of
1.78 @@ -1701,9 +1699,9 @@
1.79  subsubsection {* Generic code generator preprocessor setup *}
1.80
1.81  setup {*
1.82 -  Code_Preproc.map_pre (K HOL_basic_ss)
1.83 -  #> Code_Preproc.map_post (K HOL_basic_ss)
1.84 -  #> Code_Simp.map_ss (K HOL_basic_ss)
1.85 +  Code_Preproc.map_pre (put_simpset HOL_basic_ss)
1.86 +  #> Code_Preproc.map_post (put_simpset HOL_basic_ss)
1.87 +  #> Code_Simp.map_ss (put_simpset HOL_basic_ss)
1.88  *}
1.89
1.90  subsubsection {* Equality *}
1.91 @@ -1728,10 +1726,9 @@
1.92  declare eq_equal [code]
1.93
1.94  setup {*
1.95 -  Code_Preproc.map_pre (fn simpset =>
1.96 -    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
1.97 -      (fn thy => fn _ =>
1.98 -        fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)])
1.99 +  Code_Preproc.map_pre (fn ctxt =>
1.100 +    ctxt addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
1.101 +      (fn _ => fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)])
1.102  *}
1.103
1.104
1.105 @@ -1994,7 +1991,8 @@
1.106    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
1.107  end;
1.108
1.109 -val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps});
1.110 +fun nnf_conv ctxt =
1.111 +  Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms nnf_simps});
1.112  *}
1.113
1.114  hide_const (open) eq equal
```