# HG changeset patch
# User bulwahn
# Date 1285749195 -7200
# Node ID 05c4e9ecf5f6a1ee3227e378653bc51cb3ae5757
# Parent  cfd06840f477a6ae605ba009c9cd75434b22bd4e
improving the compilation to handle predicate arguments in higher-order argument positions

diff -r cfd06840f477 -r 05c4e9ecf5f6 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 29 10:33:15 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 29 10:33:15 2010 +0200
@@ -1696,7 +1696,13 @@
             ctxt name mode,
             Comp_Mod.funT_of compilation_modifiers mode T)))
       | (Free (s, T), Context m) =>
-        SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
+        (case (AList.lookup (op =) param_modes s) of
+          SOME mode => SOME (Free (s, Comp_Mod.funT_of compilation_modifiers m T))
+        | NONE =>
+        let
+          val bs = map (pair "x") (binder_types (fastype_of t))
+          val bounds = map Bound (rev (0 upto (length bs) - 1))
+        in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end)
       | (t, Context m) =>
         let
           val bs = map (pair "x") (binder_types (fastype_of t))