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