1.1 --- a/src/FOL/IFOL.thy	Thu May 30 08:27:51 2013 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Thu May 30 12:35:40 2013 +0200
     1.3 @@ -224,7 +224,6 @@
     1.4    done
     1.5  
     1.6  
     1.7 -(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
     1.8  lemma iffE:
     1.9    assumes major: "P <-> Q"
    1.10      and r: "P-->Q ==> Q-->P ==> R"

     2.1 --- a/src/FOLP/IFOLP.thy	Thu May 30 08:27:51 2013 +0200
     2.2 +++ b/src/FOLP/IFOLP.thy	Thu May 30 12:35:40 2013 +0200
     2.3 @@ -292,8 +292,6 @@
     2.4    done
     2.5  
     2.6  
     2.7 -(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
     2.8 -  
     2.9  schematic_lemma iffE:
    2.10    assumes "p:P <-> Q"
    2.11      and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"

     3.1 --- a/src/HOL/HOL.thy	Thu May 30 08:27:51 2013 +0200
     3.2 +++ b/src/HOL/HOL.thy	Thu May 30 12:35:40 2013 +0200
     3.3 @@ -1499,8 +1499,7 @@
     3.4                  in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
     3.5                | _ => NONE))]
     3.6      |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
     3.7 -      map (Simplifier.rewrite_rule (map Thm.symmetric
     3.8 -        @{thms induct_rulify_fallback})))))
     3.9 +      map (rewrite_rule (map Thm.symmetric @{thms induct_rulify_fallback})))))
    3.10  *}
    3.11  
    3.12  text {* Pre-simplification of induction and cases rules *}

     4.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu May 30 08:27:51 2013 +0200
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu May 30 12:35:40 2013 +0200
     4.3 @@ -51,7 +51,7 @@
     4.4    in
     4.5      thms
     4.6      |> Conjunction.intr_balanced
     4.7 -    |> Raw_Simplifier.rewrite_rule [Thm.symmetric (Thm.assume asm)]
     4.8 +    |> rewrite_rule [Thm.symmetric (Thm.assume asm)]
     4.9      |> Thm.implies_intr asm
    4.10      |> Thm.generalize ([], params) 0
    4.11      |> Axclass.unoverload thy

     5.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu May 30 08:27:51 2013 +0200
     5.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu May 30 12:35:40 2013 +0200
     5.3 @@ -554,7 +554,7 @@
     5.4  fun presimplify ctxt =
     5.5    rewrite_rule (map safe_mk_meta_eq nnf_simps)
     5.6    #> simplify (put_simpset nnf_ss ctxt)
     5.7 -  #> Raw_Simplifier.rewrite_rule @{thms Let_def [abs_def]}
     5.8 +  #> rewrite_rule @{thms Let_def [abs_def]}
     5.9  
    5.10  fun make_nnf ctxt th = case prems_of th of
    5.11      [] => th |> presimplify ctxt |> make_nnf1 ctxt

     6.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Thu May 30 08:27:51 2013 +0200
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Thu May 30 12:35:40 2013 +0200
     6.3 @@ -218,9 +218,9 @@
     6.4          fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
     6.5            |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
     6.6          val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
     6.7 -        val case_th = Raw_Simplifier.simplify true
     6.8 -          (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
     6.9 -        val prems' = maps (dest_conjunct_prem o Raw_Simplifier.simplify true tuple_rew_rules) prems
    6.10 +        val case_th =
    6.11 +          rewrite_rule (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
    6.12 +        val prems' = maps (dest_conjunct_prem o rewrite_rule tuple_rew_rules) prems
    6.13          val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
    6.14          val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
    6.15            OF (replicate nargs @{thm refl})

     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu May 30 08:27:51 2013 +0200
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu May 30 12:35:40 2013 +0200
     7.3 @@ -1025,7 +1025,7 @@
     7.4  fun peephole_optimisation thy intro =
     7.5    let
     7.6      val process =
     7.7 -      Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
     7.8 +      rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
     7.9      fun process_False intro_t =
    7.10        if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
    7.11      fun process_True intro_t =

     8.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu May 30 08:27:51 2013 +0200
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu May 30 12:35:40 2013 +0200
     8.3 @@ -213,8 +213,7 @@
     8.4            error ("unexpected specification for constant " ^ quote constname ^ ":\n"
     8.5              ^ commas (map (quote o Display.string_of_thm_global thy) specs))
     8.6        val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
     8.7 -      val intros = map (Raw_Simplifier.rewrite_rule
     8.8 -          [if_beta RS @{thm eq_reflection}]) intros
     8.9 +      val intros = map (rewrite_rule [if_beta RS @{thm eq_reflection}]) intros
    8.10        val _ = print_specs options thy "normalized intros" intros
    8.11        (*val intros = maps (split_cases thy) intros*)
    8.12        val (intros', (local_defs, thy')) = flatten_intros constname intros thy

     9.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu May 30 08:27:51 2013 +0200
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu May 30 12:35:40 2013 +0200
     9.3 @@ -127,7 +127,7 @@
     9.4            fun param_rewrite prem =
     9.5              param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
     9.6            val SOME rew_eq = find_first param_rewrite prems'
     9.7 -          val param_prem' = Raw_Simplifier.rewrite_rule
     9.8 +          val param_prem' = rewrite_rule
     9.9              (map (fn th => th RS @{thm eq_reflection})
    9.10                [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
    9.11              param_prem

    10.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu May 30 08:27:51 2013 +0200
    10.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu May 30 12:35:40 2013 +0200
    10.3 @@ -480,7 +480,7 @@
    10.4          val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
    10.5          val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
    10.6          val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
    10.7 -        val thm3 = Raw_Simplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
    10.8 +        val thm3 = rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
    10.9          val (insp, inst) =
   10.10            if ty_c = ty_d
   10.11            then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)

    11.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu May 30 08:27:51 2013 +0200
    11.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu May 30 12:35:40 2013 +0200
    11.3 @@ -38,8 +38,7 @@
    11.4      val merge = Net.merge eq
    11.5    )
    11.6  
    11.7 -  val prep =
    11.8 -    `Thm.prop_of o Simplifier.rewrite_rule [Z3_Proof_Literals.rewrite_true]
    11.9 +  val prep = `Thm.prop_of o rewrite_rule [Z3_Proof_Literals.rewrite_true]
   11.10  
   11.11    fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
   11.12    fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net

    12.1 --- a/src/HOL/Tools/record.ML	Thu May 30 08:27:51 2013 +0200
    12.2 +++ b/src/HOL/Tools/record.ML	Thu May 30 12:35:40 2013 +0200
    12.3 @@ -1748,8 +1748,7 @@
    12.4          THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
    12.5          THEN ALLGOALS (rtac @{thm refl});
    12.6        fun mk_eq thy eq_def =
    12.7 -        Simplifier.rewrite_rule
    12.8 -          [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
    12.9 +        rewrite_rule [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
   12.10        fun mk_eq_refl thy =
   12.11          @{thm equal_refl}
   12.12          |> Thm.instantiate

    13.1 --- a/src/Pure/Isar/element.ML	Thu May 30 08:27:51 2013 +0200
    13.2 +++ b/src/Pure/Isar/element.ML	Thu May 30 12:35:40 2013 +0200
    13.3 @@ -466,7 +466,7 @@
    13.4         {binding = [],
    13.5          typ = [],
    13.6          term = [Raw_Simplifier.rewrite_term thy thms []],
    13.7 -        fact = [map (Raw_Simplifier.rewrite_rule thms)]});
    13.8 +        fact = [map (rewrite_rule thms)]});
    13.9  
   13.10  
   13.11  (* transfer to theory using closure *)

    14.1 --- a/src/Pure/Isar/expression.ML	Thu May 30 08:27:51 2013 +0200
    14.2 +++ b/src/Pure/Isar/expression.ML	Thu May 30 12:35:40 2013 +0200
    14.3 @@ -671,8 +671,7 @@
    14.4          Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
    14.5  
    14.6      val conjuncts =
    14.7 -      (Drule.equal_elim_rule2 OF [body_eq,
    14.8 -        Raw_Simplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
    14.9 +      (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
   14.10        |> Conjunction.elim_balanced (length ts);
   14.11      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
   14.12        Element.prove_witness defs_ctxt t

    15.1 --- a/src/Pure/Isar/generic_target.ML	Thu May 30 08:27:51 2013 +0200
    15.2 +++ b/src/Pure/Isar/generic_target.ML	Thu May 30 12:35:40 2013 +0200
    15.3 @@ -125,7 +125,7 @@
    15.4      (*export assumes/defines*)
    15.5      val th = Goal.norm_result raw_th;
    15.6      val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
    15.7 -    val asms' = map (Raw_Simplifier.rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
    15.8 +    val asms' = map (rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
    15.9  
   15.10      (*export fixes*)
   15.11      val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);

    16.1 --- a/src/Pure/axclass.ML	Thu May 30 08:27:51 2013 +0200
    16.2 +++ b/src/Pure/axclass.ML	Thu May 30 12:35:40 2013 +0200
    16.3 @@ -292,8 +292,8 @@
    16.4  
    16.5  fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
    16.6  
    16.7 -fun unoverload thy = Raw_Simplifier.simplify true (inst_thms thy);
    16.8 -fun overload thy = Raw_Simplifier.simplify true (map Thm.symmetric (inst_thms thy));
    16.9 +fun unoverload thy = rewrite_rule (inst_thms thy);
   16.10 +fun overload thy = rewrite_rule (map Thm.symmetric (inst_thms thy));
   16.11  
   16.12  fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy);
   16.13  fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy));