# HG changeset patch
# User wenzelm
# Date 924081436 -7200
# Node ID 702527a8b2a1895da9a3e5686feaefd2194fa0d7
# Parent  87aa3e5190e08852848186daaafab5719a60369e
fixed named type infixes (actual BUG!);

diff -r 87aa3e5190e0 -r 702527a8b2a1 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Apr 13 12:39:35 1999 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Apr 14 11:17:16 1999 +0200
@@ -111,10 +111,10 @@
       let val t = name_of decl in
         (case decl of
           (_, _, NoSyn) => None
-        | (_, 2, InfixlName (sy, p)) => Some (mk_infix t sy p (p + 1) p)
-        | (_, 2, InfixrName (sy, p)) => Some (mk_infix t sy (p + 1) p p)
-        | (sy, 2, Infixl p) => Some (mk_infix t sy p (p + 1) p)
-        | (sy, 2, Infixr p) => Some (mk_infix t sy (p + 1) p p)
+        | (_, 2, InfixlName (sy, p)) => Some (mk_infix sy t p (p + 1) p)
+        | (_, 2, InfixrName (sy, p)) => Some (mk_infix sy t (p + 1) p p)
+        | (sy, 2, Infixl p) => Some (mk_infix sy t p (p + 1) p)
+        | (sy, 2, Infixr p) => Some (mk_infix sy t (p + 1) p p)
         | _ => error ("Bad mixfix declaration for type " ^ quote t))
       end;