--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Mon May 03 07:59:51 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Mon May 03 14:25:56 2010 +0200
@@ -65,7 +65,7 @@
fun specialise_intros black_list (pred, intros) pats thy =
let
- val ctxt = ProofContext.init thy
+ val ctxt = ProofContext.init_global thy
val maxidx = fold (Term.maxidx_term o prop_of) intros ~1
val pats = map (Logic.incr_indexes ([], maxidx + 1)) pats
val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt