Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Datatype/datatype_codegen.ML
changeset 33009 6b15c94e4871
parent 33007 94108ea8c568
parent 33002 f3f02f36a3e2
child 33035 15eab423e573 
--- 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
isabelle