# HG changeset patch
# User haftmann
# Date 1264175961 -3600
# Node ID 366a1a44aac22b48595268381c68a95b23ff3821
# Parent  e8cdef6d47c0a7714d3bcf673ddb3cc040078c89# Parent  807f6ce0273d1040c2ac0242e2a2b65753e4ad8d
merged

diff -r e8cdef6d47c0 -r 366a1a44aac2 NEWS
--- a/NEWS	Fri Jan 22 16:38:58 2010 +0100
+++ b/NEWS	Fri Jan 22 16:59:21 2010 +0100
@@ -12,6 +12,9 @@
 
 *** HOL ***
 
+* HOLogic.strip_psplit: types are returned in syntactic order, similar
+to other strip and tuple operations.  INCOMPATIBILITY.
+
 * Various old-style primrec specifications in the HOL theories have been
 replaced by new-style primrec, especially in theory List.  The corresponding
 constants now have authentic syntax.  INCOMPATIBILITY.
diff -r e8cdef6d47c0 -r 366a1a44aac2 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 22 16:38:58 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 22 16:59:21 2010 +0100
@@ -2636,9 +2636,9 @@
     val (body, Ts, fp) = HOLogic.strip_psplits split;
     val output_names = Name.variant_list (Term.add_free_names body [])
       (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
-    val output_frees = map2 (curry Free) output_names Ts
+    val output_frees = map2 (curry Free) output_names (rev Ts)
     val body = subst_bounds (output_frees, body)
-    val T_compr = HOLogic.mk_ptupleT fp (rev Ts)
+    val T_compr = HOLogic.mk_ptupleT fp Ts
     val output_tuple = HOLogic.mk_ptuple fp T_compr (rev output_frees)
     val (pred as Const (name, T), all_args) = strip_comb body
   in
diff -r e8cdef6d47c0 -r 366a1a44aac2 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Fri Jan 22 16:38:58 2010 +0100
+++ b/src/HOL/Tools/hologic.ML	Fri Jan 22 16:59:21 2010 +0100
@@ -426,7 +426,7 @@
 
 val strip_psplits =
   let
-    fun strip [] qs Ts t = (t, Ts, qs)
+    fun strip [] qs Ts t = (t, rev Ts, qs)
       | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
           strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
       | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
diff -r e8cdef6d47c0 -r 366a1a44aac2 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Fri Jan 22 16:38:58 2010 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Fri Jan 22 16:59:21 2010 +0100
@@ -724,7 +724,7 @@
                 let
                   val (ts1, ts2) = chop k ts;
                   val ts2' = map
-                    (fn Bound i => Term.dummy_pattern (nth Ts i) | t => t) ts2;
+                    (fn Bound i => Term.dummy_pattern (nth Ts (length Ts - i - 1)) | t => t) ts2;
                   val (ots, its) = List.partition is_Bound ts2;
                   val no_loose = forall (fn t => not (loose_bvar (t, 0)))
                 in