src/HOL/Nominal/nominal_datatype.ML
changeset 49835 31f32ec4d766
parent 49833 1d80798e8d8a
child 51122 386a117925db
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 12 18:58:20 2012 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 12 21:22:35 2012 +0200
     1.3 @@ -572,7 +572,7 @@
     1.4      val (typedefs, thy6) =
     1.5        thy4
     1.6        |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
     1.7 -          Typedef.add_typedef_global NONE
     1.8 +          Typedef.add_typedef_global
     1.9              (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
    1.10              (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
    1.11                 Const (cname, U --> HOLogic.boolT)) NONE