diff -r d6c141871b29 -r 101aefd61aac src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -64,24 +64,23 @@
 
 fun make_injs descr sorts =
   let
-    val descr' = List.concat descr;
-
-    fun make_inj T ((cname, cargs), injs) =
-      if null cargs then injs else
+    val descr' = flat descr;
+    fun make_inj T (cname, cargs) =
+      if null cargs then I else
         let
           val Ts = map (typ_of_dtyp descr' sorts) cargs;
           val constr_t = Const (cname, Ts ---> T);
           val tnames = make_tnames Ts;
           val frees = map Free (tnames ~~ Ts);
           val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
-        in (HOLogic.mk_Trueprop (HOLogic.mk_eq
+        in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
           (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
            foldr1 (HOLogic.mk_binop "op &")
-             (map HOLogic.mk_eq (frees ~~ frees')))))::injs
+             (map HOLogic.mk_eq (frees ~~ frees')))))
         end;
-
-  in map (fn (d, T) => foldr (make_inj T) [] (#3 (snd d)))
-    ((hd descr) ~~ Library.take (length (hd descr), get_rec_types descr' sorts))
+  in
+    map2 (fn d => fn T => fold_rev (make_inj T) (#3 (snd d)) [])
+      (hd descr) (Library.take (length (hd descr), get_rec_types descr' sorts))
   end;
 
 (********************************* induction **********************************)