# HG changeset patch
# User bulwahn
# Date 1269243013 -3600
# Node ID 295e1af6c8dc0da574e6aaaabe219beb6ac51e9f
# Parent  ac44e2312f0aa3fd389d1c4452923920b88b28a6
generalized split transformation in the function flattening

diff -r ac44e2312f0a -r 295e1af6c8dc src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Mar 22 08:30:12 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Mar 22 08:30:13 2010 +0100
@@ -239,12 +239,12 @@
             end)
         | Const (@{const_name "split"}, _) => 
             (let
-              val (_, [g, res]) = strip_comb t
+              val (_, g :: res :: args) = strip_comb t
               val [res1, res2] = Name.variant_list names ["res1", "res2"]
               val (T1, T2) = HOLogic.dest_prodT (fastype_of res)
               val (resv1, resv2) = (Free (res1, T1), Free (res2, T2))
             in
-              flatten' (betapplys (g, [resv1, resv2]))
+              flatten' (betapplys (g, (resv1 :: resv2 :: args)))
               (res1 :: res2 :: names,
               HOLogic.mk_Trueprop (HOLogic.mk_eq (res, HOLogic.mk_prod (resv1, resv2))) :: prems)
             end)