diff -r 6341c23baf10 -r a7a4e04b5386 src/Pure/ML/ml_syntax.ML --- a/src/Pure/ML/ml_syntax.ML Mon Mar 21 23:38:32 2011 +0100 +++ b/src/Pure/ML/ml_syntax.ML Tue Mar 22 11:14:33 2011 +0100 @@ -106,7 +106,7 @@ handle Fail _ => Symbol.explode str; val body' = if length body <= max_len then body - else take max_len body @ ["..."]; + else take (Int.max (max_len, 0)) body @ ["..."]; in Pretty.str (quote (implode (map print_char body'))) end; end;