# HG changeset patch
# User bulwahn
# Date 1274286243 -7200
# Node ID bcffdb8991674fda319e152cfc6f80c467bbdf70
# Parent  942532de16f62c23366c2b653416cfc917f8ed8d
improved behaviour of defined_functions in the predicate compiler

diff -r 942532de16f6 -r bcffdb899167 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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