src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 29 17:30:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Mar 29 17:30:53 2010 +0200
@@ -46,6 +46,9 @@
   | eq_mode (Bool, Bool) = true
   | eq_mode _ = false
 
+fun list_fun_mode [] = Bool
+  | list_fun_mode (m :: ms) = Fun (m, list_fun_mode ms)
+
 (* name: binder_modes? *)
 fun strip_fun_mode (Fun (mode, mode')) = mode :: strip_fun_mode mode'
   | strip_fun_mode Bool = []