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