# HG changeset patch
# User wenzelm
# Date 908893607 -7200
# Node ID 33ae54c0c82120c18d7fe1e2c97374a20daed922
# Parent  1f053d05f5719afce45fffe7c217ea876622befe
Syntax.max_pri;

diff -r 1f053d05f571 -r 33ae54c0c821 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Tue Oct 20 16:26:20 1998 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Tue Oct 20 16:26:47 1998 +0200
@@ -230,7 +230,7 @@
 
 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";