Syntax.max_pri;
authorwenzelm
Tue, 20 Oct 1998 16:26:47 +0200
changeset 5687 33ae54c0c821
parent 5686 1f053d05f571
child 5688 7f582495967c
Syntax.max_pri;
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";