--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu May 30 08:27:51 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu May 30 12:35:40 2013 +0200
@@ -1025,7 +1025,7 @@
fun peephole_optimisation thy intro =
let
val process =
- Raw_Simplifier.rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
+ rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
fun process_False intro_t =
if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"} then NONE else SOME intro_t
fun process_True intro_t =