diff -r 688e18023915 -r e3fd931e6095 src/Pure/sign.ML
--- 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 ();