merged
authorhaftmann
Fri Jan 22 16:59:21 2010 +0100 (2010-01-22)
changeset 34963366a1a44aac2
parent 34961 e8cdef6d47c0
parent 34962 807f6ce0273d
child 34964 4e8be3c04d37
child 34965 3b4762c1052c
child 36088 a4369989bc45
merged
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/NEWS	Fri Jan 22 16:38:58 2010 +0100
     1.2 +++ b/NEWS	Fri Jan 22 16:59:21 2010 +0100
     1.3 @@ -12,6 +12,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* HOLogic.strip_psplit: types are returned in syntactic order, similar
     1.8 +to other strip and tuple operations.  INCOMPATIBILITY.
     1.9 +
    1.10  * Various old-style primrec specifications in the HOL theories have been
    1.11  replaced by new-style primrec, especially in theory List.  The corresponding
    1.12  constants now have authentic syntax.  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 22 16:38:58 2010 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 22 16:59:21 2010 +0100
     2.3 @@ -2636,9 +2636,9 @@
     2.4      val (body, Ts, fp) = HOLogic.strip_psplits split;
     2.5      val output_names = Name.variant_list (Term.add_free_names body [])
     2.6        (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
     2.7 -    val output_frees = map2 (curry Free) output_names Ts
     2.8 +    val output_frees = map2 (curry Free) output_names (rev Ts)
     2.9      val body = subst_bounds (output_frees, body)
    2.10 -    val T_compr = HOLogic.mk_ptupleT fp (rev Ts)
    2.11 +    val T_compr = HOLogic.mk_ptupleT fp Ts
    2.12      val output_tuple = HOLogic.mk_ptuple fp T_compr (rev output_frees)
    2.13      val (pred as Const (name, T), all_args) = strip_comb body
    2.14    in
     3.1 --- a/src/HOL/Tools/hologic.ML	Fri Jan 22 16:38:58 2010 +0100
     3.2 +++ b/src/HOL/Tools/hologic.ML	Fri Jan 22 16:59:21 2010 +0100
     3.3 @@ -426,7 +426,7 @@
     3.4  
     3.5  val strip_psplits =
     3.6    let
     3.7 -    fun strip [] qs Ts t = (t, Ts, qs)
     3.8 +    fun strip [] qs Ts t = (t, rev Ts, qs)
     3.9        | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
    3.10            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
    3.11        | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
     4.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Jan 22 16:38:58 2010 +0100
     4.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Jan 22 16:59:21 2010 +0100
     4.3 @@ -724,7 +724,7 @@
     4.4                  let
     4.5                    val (ts1, ts2) = chop k ts;
     4.6                    val ts2' = map
     4.7 -                    (fn Bound i => Term.dummy_pattern (nth Ts i) | t => t) ts2;
     4.8 +                    (fn Bound i => Term.dummy_pattern (nth Ts (length Ts - i - 1)) | t => t) ts2;
     4.9                    val (ots, its) = List.partition is_Bound ts2;
    4.10                    val no_loose = forall (fn t => not (loose_bvar (t, 0)))
    4.11                  in