# HG changeset patch
# User wenzelm
# Date 1369910140 -7200
# Node ID 1105b3b5aa77345eb246fc9a6010b62b6f0299de
# Parent  ee8e3eaad24c64bb0327e0ce546eb0d45786aa32
standardized aliases;

diff -r ee8e3eaad24c -r 1105b3b5aa77 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu May 30 08:27:51 2013 +0200
+++ b/src/FOL/IFOL.thy	Thu May 30 12:35:40 2013 +0200
@@ -224,7 +224,6 @@
   done
 
 
-(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
 lemma iffE:
   assumes major: "P <-> Q"
     and r: "P-->Q ==> Q-->P ==> R"
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Thu May 30 08:27:51 2013 +0200
+++ b/src/FOLP/IFOLP.thy	Thu May 30 12:35:40 2013 +0200
@@ -292,8 +292,6 @@
   done
 
 
-(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
-  
 schematic_lemma iffE:
   assumes "p:P <-> Q"
     and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R"
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/HOL.thy	Thu May 30 12:35:40 2013 +0200
@@ -1499,8 +1499,7 @@
                 in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
               | _ => NONE))]
     |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
-      map (Simplifier.rewrite_rule (map Thm.symmetric
-        @{thms induct_rulify_fallback})))))
+      map (rewrite_rule (map Thm.symmetric @{thms induct_rulify_fallback})))))
 *}
 
 text {* Pre-simplification of induction and cases rules *}
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu May 30 12:35:40 2013 +0200
@@ -51,7 +51,7 @@
   in
     thms
     |> Conjunction.intr_balanced
-    |> Raw_Simplifier.rewrite_rule [Thm.symmetric (Thm.assume asm)]
+    |> rewrite_rule [Thm.symmetric (Thm.assume asm)]
     |> Thm.implies_intr asm
     |> Thm.generalize ([], params) 0
     |> Axclass.unoverload thy
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Thu May 30 12:35:40 2013 +0200
@@ -554,7 +554,7 @@
 fun presimplify ctxt =
   rewrite_rule (map safe_mk_meta_eq nnf_simps)
   #> simplify (put_simpset nnf_ss ctxt)
-  #> Raw_Simplifier.rewrite_rule @{thms Let_def [abs_def]}
+  #> rewrite_rule @{thms Let_def [abs_def]}
 
 fun make_nnf ctxt th = case prems_of th of
     [] => th |> presimplify ctxt |> make_nnf1 ctxt
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/HOL/Tools/Predicate_Compile/core_data.ML
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Thu May 30 12:35:40 2013 +0200
@@ -218,9 +218,9 @@
         fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
           |> snd |> Vartab.dest |> map (pairself (cterm_of thy) o term_pair_of)
         val (cases, (eqs, prems)) = apsnd (chop (nargs - nparams)) (chop n prems)
-        val case_th = Raw_Simplifier.simplify true
-          (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
-        val prems' = maps (dest_conjunct_prem o Raw_Simplifier.simplify true tuple_rew_rules) prems
+        val case_th =
+          rewrite_rule (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
+        val prems' = maps (dest_conjunct_prem o rewrite_rule tuple_rew_rules) prems
         val pats = map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop) (take nargs (prems_of case_th))
         val case_th' = Thm.instantiate ([], inst_of_matches pats) case_th
           OF (replicate nargs @{thm refl})
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu May 30 12:35:40 2013 +0200
@@ -1025,7 +1025,7 @@
 fun peephole_optimisation thy intro =
   let
     val process =
-      Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
+      rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
     fun process_False intro_t =
       if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
     fun process_True intro_t =
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu May 30 12:35:40 2013 +0200
@@ -213,8 +213,7 @@
           error ("unexpected specification for constant " ^ quote constname ^ ":\n"
             ^ commas (map (quote o Display.string_of_thm_global thy) specs))
       val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
-      val intros = map (Raw_Simplifier.rewrite_rule
-          [if_beta RS @{thm eq_reflection}]) intros
+      val intros = map (rewrite_rule [if_beta RS @{thm eq_reflection}]) intros
       val _ = print_specs options thy "normalized intros" intros
       (*val intros = maps (split_cases thy) intros*)
       val (intros', (local_defs, thy')) = flatten_intros constname intros thy
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu May 30 12:35:40 2013 +0200
@@ -127,7 +127,7 @@
           fun param_rewrite prem =
             param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem)))
           val SOME rew_eq = find_first param_rewrite prems'
-          val param_prem' = Raw_Simplifier.rewrite_rule
+          val param_prem' = rewrite_rule
             (map (fn th => th RS @{thm eq_reflection})
               [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
             param_prem
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu May 30 12:35:40 2013 +0200
@@ -480,7 +480,7 @@
         val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
         val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
         val thm2 = solve_quotient_assm ctxt (solve_quotient_assm ctxt thm1)
-        val thm3 = Raw_Simplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
+        val thm3 = rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2
         val (insp, inst) =
           if ty_c = ty_d
           then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm)
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu May 30 12:35:40 2013 +0200
@@ -38,8 +38,7 @@
     val merge = Net.merge eq
   )
 
-  val prep =
-    `Thm.prop_of o Simplifier.rewrite_rule [Z3_Proof_Literals.rewrite_true]
+  val prep = `Thm.prop_of o rewrite_rule [Z3_Proof_Literals.rewrite_true]
 
   fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
   fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/record.ML	Thu May 30 12:35:40 2013 +0200
@@ -1748,8 +1748,7 @@
         THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
         THEN ALLGOALS (rtac @{thm refl});
       fun mk_eq thy eq_def =
-        Simplifier.rewrite_rule
-          [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
+        rewrite_rule [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
       fun mk_eq_refl thy =
         @{thm equal_refl}
         |> Thm.instantiate
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/Pure/Isar/element.ML	Thu May 30 12:35:40 2013 +0200
@@ -466,7 +466,7 @@
        {binding = [],
         typ = [],
         term = [Raw_Simplifier.rewrite_term thy thms []],
-        fact = [map (Raw_Simplifier.rewrite_rule thms)]});
+        fact = [map (rewrite_rule thms)]});
 
 
 (* transfer to theory using closure *)
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/Pure/Isar/expression.ML	Thu May 30 12:35:40 2013 +0200
@@ -671,8 +671,7 @@
         Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
 
     val conjuncts =
-      (Drule.equal_elim_rule2 OF [body_eq,
-        Raw_Simplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
+      (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Conjunction.elim_balanced (length ts);
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
       Element.prove_witness defs_ctxt t
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu May 30 12:35:40 2013 +0200
@@ -125,7 +125,7 @@
     (*export assumes/defines*)
     val th = Goal.norm_result raw_th;
     val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
-    val asms' = map (Raw_Simplifier.rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
+    val asms' = map (rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms;
 
     (*export fixes*)
     val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
diff -r ee8e3eaad24c -r 1105b3b5aa77 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/Pure/axclass.ML	Thu May 30 12:35:40 2013 +0200
@@ -292,8 +292,8 @@
 
 fun get_inst_tyco consts = try (#1 o dest_Type o the_single o Consts.typargs consts);
 
-fun unoverload thy = Raw_Simplifier.simplify true (inst_thms thy);
-fun overload thy = Raw_Simplifier.simplify true (map Thm.symmetric (inst_thms thy));
+fun unoverload thy = rewrite_rule (inst_thms thy);
+fun overload thy = rewrite_rule (map Thm.symmetric (inst_thms thy));
 
 fun unoverload_conv thy = Raw_Simplifier.rewrite true (inst_thms thy);
 fun overload_conv thy = Raw_Simplifier.rewrite true (map Thm.symmetric (inst_thms thy));