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