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";