--- a/src/HOL/Nominal/nominal_datatype.ML Fri Mar 19 00:46:08 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Mar 19 00:47:23 2010 +0100
@@ -616,7 +616,7 @@
thy4
|> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
Typedef.add_typedef_global false (SOME (Binding.name name'))
- (Binding.name name, map fst tvs, mx)
+ (Binding.name name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *)
(Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
Const (cname, U --> HOLogic.boolT)) NONE
(rtac exI 1 THEN rtac CollectI 1 THEN