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