src/HOL/Tools/Datatype/datatype_aux.ML
changeset 33338 de76079f973a
parent 33317 b4534348b8fd
child 33968 f94fb13ecbb3
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 23:48:56 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Oct 29 23:49:55 2009 +0100
     1.3 @@ -162,8 +162,7 @@
     1.4      val prem' = hd (prems_of exhaustion);
     1.5      val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
     1.6      val exhaustion' = cterm_instantiate [(cterm_of thy (head_of lhs),
     1.7 -      cterm_of thy (List.foldr (fn ((_, T), t) => Abs ("z", T, t))
     1.8 -        (Bound 0) params))] exhaustion
     1.9 +      cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion
    1.10    in compose_tac (false, exhaustion', nprems_of exhaustion) i state
    1.11    end;
    1.12