src/HOL/Tools/old_primrec.ML

--- a/src/HOL/Tools/old_primrec.ML	Thu Oct 29 16:59:12 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML	Thu Oct 29 17:58:26 2009 +0100
@@ -195,7 +195,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