# HG changeset patch
# User haftmann
# Date 1248879260 -7200
# Node ID 168f31155c5e1f69da684fdabc10b00166d353d6
# Parent  65d5c5b30747810c7b4acbfc9e4074244316d239
cleaned up abstract tuple operations and named them consistently

diff -r 65d5c5b30747 -r 168f31155c5e src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Wed Jul 29 16:48:34 2009 +0200
+++ b/src/HOL/Tools/split_rule.ML	Wed Jul 29 16:54:20 2009 +0200
@@ -66,7 +66,7 @@
 (* complete splitting of partially splitted rules *)
 
 fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U
-      (ap_split T (List.concat (map HOLogic.flatten_tupleT Ts) ---> U)
+      (ap_split T (maps HOLogic.flatten_tupleT Ts ---> U)
         (incr_boundvars 1 u) $ Bound 0))
   | ap_split' _ _ u = u;
 
@@ -76,12 +76,12 @@
         val (Us', U') = strip_type T;
         val Us = Library.take (length ts, Us');
         val U = Library.drop (length ts, Us') ---> U';
-        val T' = List.concat (map HOLogic.flatten_tupleT Us) ---> U;
+        val T' = maps HOLogic.flatten_tupleT Us ---> U;
         fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
               let
                 val Ts = HOLogic.flatten_tupleT T;
                 val ys = Name.variant_list xs (replicate (length Ts) a);
-              in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
+              in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple (HOLogic.flat_tupleT_paths T) T
                 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
               end
           | mk_tuple _ x = x;