src/HOL/Tools/datatype_aux.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 16901 d649ff14096a
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -155,8 +155,8 @@
     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 sg (head_of lhs),
     1.7 -      cterm_of sg (Library.foldr (fn ((_, T), t) => Abs ("z", T, t))
     1.8 -        (params, Bound 0)))] exhaustion
     1.9 +      cterm_of sg (foldr (fn ((_, T), t) => Abs ("z", T, t))
    1.10 +        (Bound 0) params))] exhaustion
    1.11    in compose_tac (false, exhaustion', nprems_of exhaustion) i state
    1.12    end;
    1.13  
    1.14 @@ -265,8 +265,8 @@
    1.15  
    1.16  fun get_branching_types descr sorts =
    1.17    map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
    1.18 -    Library.foldl (fn (Ts', (_, cargs)) => Library.foldr op union (map (fst o strip_dtyp)
    1.19 -      cargs, Ts')) (Ts, constrs)) ([], descr));
    1.20 +    Library.foldl (fn (Ts', (_, cargs)) => foldr op union Ts' (map (fst o strip_dtyp)
    1.21 +      cargs)) (Ts, constrs)) ([], descr));
    1.22  
    1.23  fun get_arities descr = Library.foldl (fn (is, (_, (_, _, constrs))) =>
    1.24    Library.foldl (fn (is', (_, cargs)) => map (length o fst o strip_dtyp)