src/Pure/Syntax/parser.ML
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 ();