diff -r 23ceb1dc9755 -r 887e9816eea4 src/Tools/expandshort
--- a/src/Tools/expandshort	Thu Jan 18 10:38:29 1996 +0100
+++ b/src/Tools/expandshort	Fri Jan 19 16:00:22 1996 +0100
@@ -3,6 +3,7 @@
 #Shell script to expand shorthand goal commands
 #  ALSO contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
 #     rewrite_goals_tac on 1-element lists
+#  ALSO expands tabs, since they are now forbidden in strings.
 #
 # Usage:
 #    expandshort FILE1 ... FILEn
@@ -26,6 +27,6 @@
 s/eresolve_tac *\[\([a-zA-Z0-9_]*\)\] */etac \1 /g
 s/resolve_tac *\[\([a-zA-Z0-9_]*\)\] */rtac \1 /g
 s/rewrite_goals_tac *\[\([a-zA-Z0-9_]*\)\]\( *\)/rewtac \1\2/g
-' $f~~ > $f
+' $f~~ | expand > $f
 done
 echo Finished.