lib/Tools/expandshort

--- a/lib/Tools/expandshort	Thu Feb 06 17:52:40 1997 +0100
+++ b/lib/Tools/expandshort	Thu Feb 06 18:22:21 1997 +0100
@@ -15,7 +15,7 @@
   echo "  Expand shorthand goal commands in FILES.  Also contracts uses of"
   echo "  resolve_tac, dresolve_tac, eresolve_tac, rewrite_goals_tac on"
   echo "  1-element lists; furthermore expands tabs, since they are now"
-  echo "  forbidden in strings."
+  echo "  forbidden in ML string constants."
   echo
   echo "  Renames old versions of FILES by appending \"~~\"."
   echo