# HG changeset patch # User wenzelm # Date 1369130585 -7200 # Node ID 6225d5b308f903d7f6a52e028e14298076d8c712 # Parent 6c38df1d294af3a7d16451f9a330295f0c357551 make SML/NJ happy; diff -r 6c38df1d294a -r 6225d5b308f9 src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Tue May 21 11:01:14 2013 +0200 +++ b/src/Tools/Code/code_printer.ML Tue May 21 12:03:05 2013 +0200 @@ -488,17 +488,17 @@ val parse_fixity = (@{keyword "infix"} >> K X) || (@{keyword "infixl"} >> K L) || (@{keyword "infixr"} >> K R) -val parse_mixfix = - Parse.string >> read_mixfix +fun parse_mixfix x = + (Parse.string >> read_mixfix || parse_fixity -- Parse.nat -- Parse.string - >> (fn ((fixity, i), s) => read_infix (fixity, i) s); + >> (fn ((fixity, i), s) => read_infix (fixity, i) s)) x; fun syntax_of_mixfix of_plain of_printer prep_arg (BR, [String s]) = of_plain s | syntax_of_mixfix of_plain of_printer prep_arg (fixity, mfx) = of_printer (printer_of_mixfix prep_arg (fixity, mfx)); -val parse_tyco_syntax = - parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o str) s)) I I; +fun parse_tyco_syntax x = + (parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o str) s)) I I) x; val parse_const_syntax = parse_mixfix >> syntax_of_mixfix plain_const_syntax simple_const_syntax fst;