src/HOL/Tools/datatype_aux.ML

     val (_, Type (tname, _)) = hd (rev params);
     val exhaustion = lift_rule (state, i) (exh_thm_of tname);
     val prem' = hd (prems_of exhaustion);
     val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
     val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),
-      cterm_of sg (Library.foldr (fn ((_, T), t) => Abs ("z", T, t))
-        (params, Bound 0)))] exhaustion
+      cterm_of sg (foldr (fn ((_, T), t) => Abs ("z", T, t))
+        (Bound 0) params))] exhaustion
   in compose_tac (false, exhaustion', nprems_of exhaustion) i state
   end;
 
 (* handling of distinctness theorems *)
 

 
 (* get all branching types *)
 
 fun get_branching_types descr sorts =
   map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
-    Library.foldl (fn (Ts', (_, cargs)) => Library.foldr op union (map (fst o strip_dtyp)
-      cargs, Ts')) (Ts, constrs)) ([], descr));
+    Library.foldl (fn (Ts', (_, cargs)) => foldr op union Ts' (map (fst o strip_dtyp)
+      cargs)) (Ts, constrs)) ([], descr));
 
 fun get_arities descr = Library.foldl (fn (is, (_, (_, _, constrs))) =>
   Library.foldl (fn (is', (_, cargs)) => map (length o fst o strip_dtyp)
     (List.filter is_rec_type cargs) union is') (is, constrs)) ([], descr);