# HG changeset patch
# User haftmann
# Date 1264175811 -3600
# Node ID 807f6ce0273d1040c2ac0242e2a2b65753e4ad8d
# Parent  e1b8f273640415617663d88ded5403cd6ca6d7dc
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)

diff -r e1b8f2736404 -r 807f6ce0273d NEWS
--- a/NEWS	Fri Jan 22 13:39:00 2010 +0100
+++ b/NEWS	Fri Jan 22 16:56:51 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 e1b8f2736404 -r 807f6ce0273d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 22 13:39:00 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 22 16:56:51 2010 +0100
@@ -2562,9 +2562,9 @@
     val t_eval = if null outargs then t_pred else
       let
         val outargs_bounds = map (fn Bound i => i) outargs;
-        val outargsTs = map (nth Ts) outargs_bounds;
+        val outargsTs = map (fn i => nth Ts (length Ts - i - 1)) outargs_bounds;
         val T_pred = HOLogic.mk_tupleT outargsTs;
-        val T_compr = HOLogic.mk_ptupleT fp (rev Ts);
+        val T_compr = HOLogic.mk_ptupleT fp Ts;
         val k = length outargs - 1;
         val arrange_bounds = map_index (fn (i, j) => (k-i, k-j)) outargs_bounds
           |> sort (prod_ord (K EQUAL) int_ord)
diff -r e1b8f2736404 -r 807f6ce0273d src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Fri Jan 22 13:39:00 2010 +0100
+++ b/src/HOL/Tools/hologic.ML	Fri Jan 22 16:56:51 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 e1b8f2736404 -r 807f6ce0273d src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Fri Jan 22 13:39:00 2010 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Fri Jan 22 16:56:51 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