--- 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"
--- 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"
--- 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 *}
--- 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
--- 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
--- 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})
--- 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 =
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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 *)
--- 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
--- 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' []);
--- 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));