src/HOL/Nominal/nominal_primrec.ML

--- a/src/HOL/Nominal/nominal_primrec.ML	Thu Oct 29 16:59:12 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Oct 29 17:58:26 2009 +0100
@@ -193,7 +193,7 @@
      NONE =>
        let
          val dummy_fns = map (fn (_, cargs) => Const (@{const_name 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