src/Pure/sign.ML
changeset 1580 e3fd931e6095
parent 1576 af8f43f742a0
child 1810 0eef167ebe1b
--- a/src/Pure/sign.ML	Thu Mar 14 16:40:18 1996 +0100
+++ b/src/Pure/sign.ML	Fri Mar 15 12:01:19 1996 +0100
@@ -315,7 +315,7 @@
     fun warn() =
       if length ts > 1 andalso length ts <= !Syntax.ambiguity_level
       then (*no warning shown yet*)
-           writeln "Warning: Currently parsed input \
+           warning "Currently parsed input \
                    \produces more than one parse tree.\n\
                    \For more information lower Syntax.ambiguity_level."
       else ();