# HG changeset patch
# User berghofe
# Date 1224444055 -7200
# Node ID f6e1b2beb766b76fca8d01315628e1c0d962fe17
# Parent  188e9557c57295e32a28e62bc0f7c2b6ee757334
Names of variables in perm_eqs are now chosen more carefully to avoid
clashes with name "pi".

diff -r 188e9557c572 -r f6e1b2beb766 src/HOL/Nominal/nominal_package.ML
--- 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) =