diff -r a701907d621e -r 1c5bc387bd4c src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 08 23:04:18 2014 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 08 23:04:18 2014 +0200
@@ -574,7 +574,7 @@
     val (typedefs, thy6) =
       thy4
       |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
-          Typedef.add_typedef_global
+          Typedef.add_typedef_global false
             (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
             (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
                Const (cname, U --> HOLogic.boolT)) NONE