--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Dec 13 23:53:02 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Dec 14 17:28:05 2013 +0100
@@ -1017,8 +1017,9 @@
fun peephole_optimisation thy intro =
let
+ val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
val process =
- rewrite_rule (Predicate_Compile_Simps.get (Proof_Context.init_global thy))
+ rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt)
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 =