--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon May 03 14:25:56 2010 +0200
@@ -778,7 +778,7 @@
let
val (_, args) = strip_comb atom
in rewrite_args args end
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
val intro_t = prop_of intro'
val concl = Logic.strip_imp_concl intro_t
@@ -860,7 +860,8 @@
fun peephole_optimisation thy intro =
let
- val process = MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.init thy))
+ val process =
+ MetaSimplifier.rewrite_rule (Predicate_Compile_Simps.get (ProofContext.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 =