src/Pure/sign.ML

     val ct = const_type sg;
 
     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 ();
 
     datatype result = One of int * term * (indexname * typ) list