--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Aug 16 20:27:51 2014 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Aug 16 20:46:59 2014 +0200
@@ -1042,7 +1042,7 @@
let
val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *)
val process =
- rewrite_rule ctxt (Predicate_Compile_Simps.get ctxt)
+ rewrite_rule ctxt (Named_Theorems.get ctxt @{named_theorems code_pred_simp})
fun process_False intro_t =
if member (op =) (Logic.strip_imp_prems intro_t) @{prop "False"}
then NONE else SOME intro_t