refer to regular structure Simplifier;
authorwenzelm
Fri Dec 17 13:45:43 2010 +0100 (2010-12-17)
changeset 41225bd4ecd48c21f
parent 41224 8a104c2a186f
child 41226 adcb9a1198e7
refer to regular structure Simplifier;
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Predicate_Compile/core_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/lin_arith.ML
src/Tools/Code/code_simp.ML
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Fri Dec 17 13:12:58 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Fri Dec 17 13:45:43 2010 +0100
     1.3 @@ -312,7 +312,7 @@
     1.4  
     1.5          val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
     1.6            |> Goal.init
     1.7 -          |> (MetaSimplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
     1.8 +          |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
     1.9                THEN CONVERSION ind_rulify 1)
    1.10            |> Seq.hd
    1.11            |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
     2.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Dec 17 13:12:58 2010 +0100
     2.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Dec 17 13:45:43 2010 +0100
     2.3 @@ -297,7 +297,7 @@
     2.4          else Conv.all_conv
     2.5        | _ => Conv.all_conv)
     2.6  
     2.7 -fun ss_only ths = MetaSimplifier.clear_ss HOL_basic_ss addsimps ths
     2.8 +fun ss_only ths = Simplifier.clear_ss HOL_basic_ss addsimps ths
     2.9  
    2.10  val cheat_choice =
    2.11    @{prop "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)"}
     3.1 --- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Dec 17 13:12:58 2010 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Fri Dec 17 13:45:43 2010 +0100
     3.3 @@ -237,7 +237,7 @@
     3.4        (PEEK nprems_of
     3.5          (fn n =>
     3.6            ALLGOALS (fn i =>
     3.7 -            MetaSimplifier.rewrite_goal_tac [@{thm split_paired_all}] i
     3.8 +            Simplifier.rewrite_goal_tac [@{thm split_paired_all}] i
     3.9              THEN (SUBPROOF (instantiate i n) ctxt i))))
    3.10    in
    3.11      Goal.prove ctxt (Term.add_free_names cases_rule []) [] cases_rule (fn _ => tac)
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Dec 17 13:12:58 2010 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Fri Dec 17 13:45:43 2010 +0100
     4.3 @@ -83,7 +83,7 @@
     4.4          let
     4.5            val prems' = maps dest_conjunct_prem (take nargs prems)
     4.6          in
     4.7 -          MetaSimplifier.rewrite_goal_tac
     4.8 +          Simplifier.rewrite_goal_tac
     4.9              (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    4.10          end) ctxt 1
    4.11      | Abs _ => raise Fail "prove_param: No valid parameter term"
    4.12 @@ -184,7 +184,7 @@
    4.13                  let
    4.14                    val prems' = maps dest_conjunct_prem (take nargs prems)
    4.15                  in
    4.16 -                  MetaSimplifier.rewrite_goal_tac
    4.17 +                  Simplifier.rewrite_goal_tac
    4.18                      (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    4.19                  end
    4.20               THEN REPEAT_DETERM (rtac @{thm refl} 1))
    4.21 @@ -225,7 +225,7 @@
    4.22                let
    4.23                  val prems' = maps dest_conjunct_prem (take nargs prems)
    4.24                in
    4.25 -                MetaSimplifier.rewrite_goal_tac
    4.26 +                Simplifier.rewrite_goal_tac
    4.27                    (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
    4.28                end) ctxt 1
    4.29        THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
     5.1 --- a/src/HOL/Tools/TFL/rules.ML	Fri Dec 17 13:12:58 2010 +0100
     5.2 +++ b/src/HOL/Tools/TFL/rules.ML	Fri Dec 17 13:45:43 2010 +0100
     5.3 @@ -714,7 +714,7 @@
     5.4                   else
     5.5                   let val tych = cterm_of thy
     5.6                       val ants1 = map tych ants
     5.7 -                     val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
     5.8 +                     val ss' = Simplifier.add_prems (map ASSUME ants1) ss
     5.9                       val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
    5.10                          (false,true,false) (prover used') ss' (tych Q)
    5.11                        handle Utils.ERR _ => Thm.reflexive (tych Q)
     6.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Dec 17 13:12:58 2010 +0100
     6.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Dec 17 13:45:43 2010 +0100
     6.3 @@ -807,7 +807,7 @@
     6.4    add_discrete_type @{type_name nat};
     6.5  
     6.6  fun add_arith_facts ss =
     6.7 -  add_prems (Arith_Data.get_arith_facts (MetaSimplifier.the_context ss)) ss;
     6.8 +  Simplifier.add_prems (Arith_Data.get_arith_facts (Simplifier.the_context ss)) ss;
     6.9  
    6.10  val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
    6.11  
     7.1 --- a/src/Tools/Code/code_simp.ML	Fri Dec 17 13:12:58 2010 +0100
     7.2 +++ b/src/Tools/Code/code_simp.ML	Fri Dec 17 13:45:43 2010 +0100
     7.3 @@ -24,7 +24,7 @@
     7.4  (
     7.5    type T = simpset;
     7.6    val empty = empty_ss;
     7.7 -  fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
     7.8 +  fun extend ss = Simplifier.inherit_context empty_ss ss;
     7.9    val merge = merge_ss;
    7.10  );
    7.11