# HG changeset patch
# User wenzelm
# Date 876401724 -7200
# Node ID 7e8847f8f3a4420953029b13e01821edeab91abb
# Parent  b0dc68aa1b6ac0b3d1e5892eaea8ac8cc1fe3a82
fixed infix syntax;

diff -r b0dc68aa1b6a -r 7e8847f8f3a4 src/Pure/Syntax/mixfix.ML
--- 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