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 ();