--- a/src/HOL/Nominal/nominal_datatype.ML Sat Mar 13 14:42:16 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sat Mar 13 14:43:04 2010 +0100
@@ -615,7 +615,7 @@
val (typedefs, thy6) =
thy4
|> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
- Typedef.add_typedef false (SOME (Binding.name name'))
+ Typedef.add_typedef_global false (SOME (Binding.name name'))
(Binding.name name, map fst tvs, mx)
(Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
Const (cname, U --> HOLogic.boolT)) NONE