Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Names of variables in perm_eqs are now chosen more carefully to avoid
authorberghofe
Sun, 19 Oct 2008 21:20:55 +0200
changeset 28641 f6e1b2beb766
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 file | annotate | diff | comparison | revisions 
--- 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) =
isabelle