src/Pure/Syntax/mixfix.ML
changeset 3815 7e8847f8f3a4
parent 3690 3f7053bf4237
child 3829 d7333ef9e72c
--- 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