# HG changeset patch
# User wenzelm
# Date 1292589943 -3600
# Node ID bd4ecd48c21f3c05128542792fb0939f37f7849a
# Parent  8a104c2a186f394f85d0acd4c822967c73498e7d
refer to regular structure Simplifier;

diff -r 8a104c2a186f -r bd4ecd48c21f src/HOL/Tools/Function/induction_schema.ML
--- 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)
diff -r 8a104c2a186f -r bd4ecd48c21f src/HOL/Tools/Meson/meson_clausify.ML
--- 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)"}
diff -r 8a104c2a186f -r bd4ecd48c21f src/HOL/Tools/Predicate_Compile/core_data.ML
--- 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)
diff -r 8a104c2a186f -r bd4ecd48c21f src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
--- 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)
diff -r 8a104c2a186f -r bd4ecd48c21f src/HOL/Tools/TFL/rules.ML
--- 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)
diff -r 8a104c2a186f -r bd4ecd48c21f src/HOL/Tools/lin_arith.ML
--- 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;
 
diff -r 8a104c2a186f -r bd4ecd48c21f src/Tools/Code/code_simp.ML
--- 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;
 );