diff -r 6a72af4e84b8 -r b4534348b8fd src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Thu Oct 29 16:59:12 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Thu Oct 29 17:58:26 2009 +0100
@@ -178,7 +178,7 @@
      NONE =>
        let
          val dummy_fns = map (fn (_, cargs) => Const ("HOL.undefined",
-           replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
+           replicate (length cargs + length (filter is_rec_type cargs))
              dummyT ---> HOLogic.unitT)) constrs;
          val _ = warning ("No function definition for datatype " ^ quote tname)
        in