# HG changeset patch
# User bulwahn
# Date 1284637757 -7200
# Node ID 3cb3b1668c5dafedae7af83b2b89d31fda5d59ec
# Parent  139c694299f64929166a5e68333b8d28684b5045
improving replacing higher order arguments to work with tuples

diff -r 139c694299f6 -r 3cb3b1668c5d src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Sep 16 13:49:14 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Sep 16 13:49:17 2010 +0200
@@ -333,11 +333,20 @@
               ((full_constname, [definition])::new_defs, thy'))
           end
         | replace_abs_arg arg (new_defs, thy) =
-          if (is_predT (fastype_of arg)) then
+          if is_some (try HOLogic.dest_prodT (fastype_of arg)) then
+            (case try HOLogic.dest_prod arg of
+              SOME (t1, t2) =>
+                (new_defs, thy)
+                |> process constname t1 
+                ||>> process constname t2
+                |>> HOLogic.mk_prod
+            | NONE => (warning ("Replacing higher order arguments " ^
+              "is not applied in an undestructable product type"); (arg, (new_defs, thy))))
+          else 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
           (map Envir.beta_eta_contract args) (new_defs, thy)
       in