Names of variables in perm_eqs are now chosen more carefully to avoid
authorberghofe
Sun Oct 19 21:20:55 2008 +0200 (2008-10-19)
changeset 28641f6e1b2beb766
parent 28640 188e9557c572
child 28642 658b598d8af4
Names of variables in perm_eqs are now chosen more carefully to avoid
clashes with name "pi".
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Sun Oct 19 21:19:27 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sun Oct 19 21:20:55 2008 +0200
     1.3 @@ -272,7 +272,7 @@
     1.4        in map (fn (cname, dts) =>
     1.5          let
     1.6            val Ts = map (typ_of_dtyp descr sorts') dts;
     1.7 -          val names = DatatypeProp.make_tnames Ts;
     1.8 +          val names = Name.variant_list ["pi"] (DatatypeProp.make_tnames Ts);
     1.9            val args = map Free (names ~~ Ts);
    1.10            val c = Const (cname, Ts ---> T);
    1.11            fun perm_arg (dt, x) =