# HG changeset patch
# User wenzelm
# Date 1008365391 -3600
# Node ID ab14b29dfc6d7ff9c160616a61ca883e5ede28ef
# Parent  901c6c4779076f78caf4ad396541958f8ef9db86
removed special treatment of "_" in syntax (now covered by \<index> arg);

diff -r 901c6c477907 -r ab14b29dfc6d src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Dec 14 22:29:11 2001 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Dec 14 22:29:51 2001 +0100
@@ -126,8 +126,6 @@
   | mixfix_args (Delimfix sy) = SynExt.mfix_args sy
   | mixfix_args (*infix or binder*) _ = 2;
 
-fun maxpris sy = replicate (SynExt.mfix_args sy) 0;
-
 
 (* syn_ext_types *)
 
@@ -137,7 +135,7 @@
 
     fun mk_infix sy t p1 p2 p3 =
       SynExt.Mfix ("(_ " ^ sy ^ "/ _)",
-        [SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, p1 :: maxpris sy @ [p2], p3);
+        [SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, [p1, p2], p3);
 
     fun mfix_of decl =
       let val t = name_of decl in
@@ -165,7 +163,7 @@
 
     fun mk_infix sy ty c p1 p2 p3 =
       [SynExt.Mfix ("op " ^ sy, ty, c, [], SynExt.max_pri),
-       SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, p1 :: maxpris sy @ [p2], p3)];
+       SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
 
     fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
           [Type ("idts", []), ty2] ---> ty3
@@ -237,7 +235,7 @@
   ("_DDDOT",       "logic",                         Delimfix "..."),
   ("_constify",    "num => num_const",              Delimfix "_"),
   ("_index",       "num_const => index",            Delimfix "\\<^sub>_"),
-  ("_indexvar",    "index",                         Delimfix "\\<index>"),
+  ("_indexvar",    "index",                         Delimfix "'\\<index>"),
   ("_noindex",     "index",                         Delimfix ""),
   ("_struct",      "index => logic",                Delimfix "\\<struct>_")];