--- 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.
--- 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
--- 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
--- 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