# HG changeset patch
# User bulwahn
# Date 1269876653 -7200
# Node ID d82682936c529516cb10f68908633905898b7eff
# Parent  ee84eac072902fe8de342535e44c422a6eeb9c66
adding registration of functions in the function flattening

diff -r ee84eac07290 -r d82682936c52 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 = []
diff -r ee84eac07290 -r d82682936c52 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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 *)
 
diff -r ee84eac07290 -r d82682936c52 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- 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 =