diff -r 3d4bfc7f6363 -r f9fd69d96c4e src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Fri Dec 01 17:22:30 2006 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Fri Dec 01 17:22:31 2006 +0100
@@ -377,7 +377,7 @@
         val ts = map (fn ((r, s), T) => List.nth (size_consts, dest_DtRec r) $
           Free (s, T)) (recs ~~ rec_tnames ~~ recTs);
         val t = if ts = [] then HOLogic.zero else
-          foldl1 plus (ts @ [HOLogic.mk_nat 1])
+          foldl1 plus (ts @ [HOLogic.Suc_zero])
       in
         HOLogic.mk_Trueprop (HOLogic.mk_eq (size_const $
           list_comb (Const (cname, Ts ---> T), map Free (tnames ~~ Ts)), t))