--- a/src/HOL/Tools/Function/induction_schema.ML Fri Dec 17 13:12:58 2010 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Fri Dec 17 13:45:43 2010 +0100
@@ -312,7 +312,7 @@
val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
|> Goal.init
- |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
+ |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
THEN CONVERSION ind_rulify 1)
|> Seq.hd
|> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Dec 17 13:12:58 2010 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Fri Dec 17 13:45:43 2010 +0100
@@ -297,7 +297,7 @@
else Conv.all_conv
| _ => Conv.all_conv)
-fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths
+fun ss_only ths = Simplifier.clear_ss HOL_basic_ss addsimps ths
val cheat_choice =
@{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"}
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Fri Dec 17 13:12:58 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Fri Dec 17 13:45:43 2010 +0100
@@ -237,7 +237,7 @@
(PEEK nprems_of
(fn n =>
ALLGOALS (fn i =>
- MetaSimplifier.rewrite_goal_tac [@{thm split_paired_all}] i
+ Simplifier.rewrite_goal_tac [@{thm split_paired_all}] i
THEN (SUBPROOF (instantiate i n) ctxt i))))
in
Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Dec 17 13:12:58 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Fri Dec 17 13:45:43 2010 +0100
@@ -83,7 +83,7 @@
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
- MetaSimplifier.rewrite_goal_tac
+ Simplifier.rewrite_goal_tac
(map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end) ctxt 1
| Abs _ => raise Fail "prove_param: No valid parameter term"
@@ -184,7 +184,7 @@
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
- MetaSimplifier.rewrite_goal_tac
+ Simplifier.rewrite_goal_tac
(map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end
THEN REPEAT_DETERM (rtac @{thm refl} 1))
@@ -225,7 +225,7 @@
let
val prems' = maps dest_conjunct_prem (take nargs prems)
in
- MetaSimplifier.rewrite_goal_tac
+ Simplifier.rewrite_goal_tac
(map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
end) ctxt 1
THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
--- a/src/HOL/Tools/TFL/rules.ML Fri Dec 17 13:12:58 2010 +0100
+++ b/src/HOL/Tools/TFL/rules.ML Fri Dec 17 13:45:43 2010 +0100
@@ -714,7 +714,7 @@
else
let val tych = cterm_of thy
val ants1 = map tych ants
- val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
+ val ss' = Simplifier.add_prems (map ASSUME ants1) ss
val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
(false,true,false) (prover used') ss' (tych Q)
handle Utils.ERR _ => Thm.reflexive (tych Q)
--- a/src/HOL/Tools/lin_arith.ML Fri Dec 17 13:12:58 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML Fri Dec 17 13:45:43 2010 +0100
@@ -807,7 +807,7 @@
add_discrete_type @{type_name nat};
fun add_arith_facts ss =
- add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
+ Simplifier.add_prems (Arith_Data.get_arith_facts (Simplifier.the_context ss)) ss;
val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
--- a/src/Tools/Code/code_simp.ML Fri Dec 17 13:12:58 2010 +0100
+++ b/src/Tools/Code/code_simp.ML Fri Dec 17 13:45:43 2010 +0100
@@ -24,7 +24,7 @@
(
type T = simpset;
val empty = empty_ss;
- fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
+ fun extend ss = Simplifier.inherit_context empty_ss ss;
val merge = merge_ss;
);