src/Pure/Thy/thy_parse.ML
changeset 5687 33ae54c0c821
parent 5248 6b04b9a88c21
child 5905 68cdba6c178f
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Oct 20 16:26:20 1998 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Oct 20 16:26:47 1998 +0200
     1.3 @@ -230,7 +230,7 @@
     1.4  
     1.5  val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
     1.6  
     1.7 -val mixfix = string -- !! (opt_pris -- optional nat "max_pri")
     1.8 +val mixfix = string -- !! (opt_pris -- optional nat "Syntax.max_pri")
     1.9    >> (cat "Mixfix" o mk_triple2);
    1.10  
    1.11  fun opt_syn fx = optional ("(" $$-- fx --$$ ")") "NoSyn";