changeset 1580 | e3fd931e6095 |
parent 1507 | f600215b6ea7 |
child 2186 | 35ade4941904 |
--- 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 ();