changeset 28641 | f6e1b2beb766 |
parent 28373 | 5e2c526cfaf0 |
child 28662 | 64ab5bb68d4c |
--- a/src/HOL/Nominal/nominal_package.ML Sun Oct 19 21:19:27 2008 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Sun Oct 19 21:20:55 2008 +0200 @@ -272,7 +272,7 @@ in map (fn (cname, dts) => let val Ts = map (typ_of_dtyp descr sorts') dts; - val names = DatatypeProp.make_tnames Ts; + val names = Name.variant_list ["pi"] (DatatypeProp.make_tnames Ts); val args = map Free (names ~~ Ts); val c = Const (cname, Ts ---> T); fun perm_arg (dt, x) =