diff -r b0ff69f0a248 -r 6b15c94e4871 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Oct 20 08:10:47 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Oct 20 10:46:42 2009 +0200
@@ -20,7 +20,7 @@
     val (_, _, constrs) = the (AList.lookup (op =) descr i);
     fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
           then NONE
-          else Option.map (curry op + 1 o snd) (find_nonempty descr (i::is) i)
+          else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
       | arg_nonempty _ = SOME 0;
     fun max xs = Library.foldl
       (fn (NONE, _) => NONE