diff -r 6ed6112f0a95 -r bafd82950e24 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
--- 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