# HG changeset patch
# User bulwahn
# Date 1257240245 -3600
# Node ID a9b6497391b05969bcb42069f3900654fb599f34
# Parent  d9a25a87da4a226c1531daa79857bc5f220a8543
recursively replacing abstractions by new definitions in the predicate compiler

diff -r d9a25a87da4a -r a9b6497391b0 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Nov 02 18:49:53 2009 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Tue Nov 03 10:24:05 2009 +0100
@@ -141,7 +141,6 @@
     fun process constname atom (new_defs, thy) =
       let
         val (pred, args) = strip_comb atom
-        val abs_args = filter is_Abs args
         fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) =
           let
             val vars = map Var (Term.add_vars abs_arg [])
@@ -160,7 +159,12 @@
           in
             (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy'))
           end
-        | replace_abs_arg arg (new_defs, thy) = (arg, (new_defs, thy))
+        | replace_abs_arg arg (new_defs, thy) =
+          if (is_predT (fastype_of arg)) then
+            process constname arg (new_defs, thy)
+          else
+            (arg, (new_defs, thy))
+        
         val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy)
       in
         (list_comb (pred, args'), (new_defs', thy'))