1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 17:39:22 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:03 2010 +0200
     1.3 @@ -268,8 +268,9 @@
     1.4  
     1.5  val all_random_modes_of = all_modes_of Random
     1.6  
     1.7 -fun defined_functions compilation thy name =
     1.8 -  AList.defined (op =) (#function_names (the_pred_data thy name)) compilation
     1.9 +fun defined_functions compilation thy name = case lookup_pred_data thy name of
    1.10 +    NONE => false
    1.11 +  | SOME data => AList.defined (op =) (#function_names data) compilation
    1.12  
    1.13  fun lookup_predfun_data thy name mode =
    1.14    Option.map rep_predfun_data