src/Pure/Thy/thy_parse.ML

   !! (string -- (("[" $$-- nat --$$ "]") -- nat || nat >> (fn n => (n, n))))
     >> (cat "Binder" o mk_triple2);
 
 val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
 
-val mixfix = string -- !! (opt_pris -- optional nat "max_pri")
+val mixfix = string -- !! (opt_pris -- optional nat "Syntax.max_pri")
   >> (cat "Mixfix" o mk_triple2);
 
 fun opt_syn fx = optional ("(" $$-- fx --$$ ")") "NoSyn";
 
 val opt_infix = opt_syn (infxl || infxr);