--- 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 = []
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 29 17:30:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 29 17:30:53 2010 +0200
@@ -736,7 +736,7 @@
Alt_Names_Data.map (Symtab.insert_list (op =) (pred_name, (mode, fun_name)))
fun alternative_function_of thy pred_name mode =
- AList.lookup (op =) (Symtab.lookup_list (Alt_Names_Data.get thy) pred_name) mode
+ AList.lookup eq_mode (Symtab.lookup_list (Alt_Names_Data.get thy) pred_name) mode
(* datastructures and setup for generic compilation *)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Mar 29 17:30:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Mon Mar 29 17:30:53 2010 +0200
@@ -327,8 +327,14 @@
val thy'' = Fun_Pred.map
(fold Item_Net.update (map (apfst Logic.varify_global)
(distinct (op =) funs ~~ (#preds ind_result)))) thy'
+ fun functional_mode_of T =
+ list_fun_mode (replicate (length (binder_types T)) Input @ [Output])
+ val thy''' = fold
+ (fn (predname, Const (name, T)) => Predicate_Compile_Core.register_alternative_function
+ predname (functional_mode_of T) name)
+ (prednames ~~ distinct (op =) funs) thy''
in
- (specs, thy'')
+ (specs, thy''')
end
fun rewrite_intro thy intro =