diff -r 688e18023915 -r e3fd931e6095 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Thu Mar 14 16:40:18 1996 +0100 +++ b/src/Pure/Syntax/parser.ML Fri Mar 15 12:01:19 1996 +0100 @@ -752,7 +752,7 @@ val dummy = if not (!warned) andalso length (new_states @ States) > (!branching_level) then - (writeln "Warning: Currently parsed expression could be \ + (warning "Currently parsed expression could be \ \extremely ambiguous."; warned := true) else ();