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.
fixed infix syntax;
authorwenzelm
Thu, 09 Oct 1997 14:55:24 +0200
changeset 3815 7e8847f8f3a4
parent 3814 b0dc68aa1b6a
child 3816 7e1b695bcc5e
fixed infix syntax;
src/Pure/Syntax/mixfix.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Syntax/mixfix.ML	Thu Oct 09 14:55:05 1997 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Thu Oct 09 14:55:24 1997 +0200
@@ -116,8 +116,8 @@
     fun name_of (c, _, mx) = const_name c mx;
 
     fun mk_infix sy ty c p1 p2 p3 =
-      [Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3),
-       Mfix ("op " ^ sy, ty, c, [], max_pri)];
+      [Mfix ("op " ^ sy, ty, c, [], max_pri),
+       Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
 
     fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
           [Type ("idts", []), ty2] ---> ty3
isabelle