# 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