src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 41228 e1fce873b814
parent 40844 5895c525739d
child 42094 e6867e9c6d10
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Dec 17 16:25:21 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Dec 17 17:08:56 2010 +0100
     1.3 @@ -969,7 +969,7 @@
     1.4      val Tcons = datatype_names_of_case_name thy case_name
     1.5      val ths = maps (instantiated_case_rewrites thy) Tcons
     1.6    in
     1.7 -    MetaSimplifier.rewrite_term thy
     1.8 +    Raw_Simplifier.rewrite_term thy
     1.9        (map (fn th => th RS @{thm eq_reflection}) ths) [] t
    1.10    end
    1.11  
    1.12 @@ -1044,7 +1044,7 @@
    1.13  fun peephole_optimisation thy intro =
    1.14    let
    1.15      val process =
    1.16 -      MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy))
    1.17 +      Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init_global thy))
    1.18      fun process_False intro_t =
    1.19        if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
    1.20      fun process_True intro_t =