src/HOL/Tools/Predicate_Compile/predicate_compile.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed May 19 18:24:04 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed May 19 18:24:05 2010 +0200
@@ -74,7 +74,8 @@
   end
 
 fun preprocess_strong_conn_constnames options gr ts thy =
-  if forall (fn (Const (c, _)) => Predicate_Compile_Core.is_registered thy c) ts then
+  if forall (fn (Const (c, _)) =>
+      Predicate_Compile_Core.is_registered (ProofContext.init_global thy) c) ts then
     thy
   else
     let