src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 52230 1105b3b5aa77
parent 51717 9e7d1c139569
child 53887 ee91bd2a506a
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu May 30 08:27:51 2013 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu May 30 12:35:40 2013 +0200
     1.3 @@ -1025,7 +1025,7 @@
     1.4  fun peephole_optimisation thy intro =
     1.5    let
     1.6      val process =
     1.7 -      Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
     1.8 +      rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
     1.9      fun process_False intro_t =
    1.10        if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
    1.11      fun process_True intro_t =