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