diff -r 6db93e6f1b11 -r a3262b93c1d2 src/Tools/expandshort
--- a/src/Tools/expandshort	Thu Sep 26 17:15:19 1996 +0200
+++ b/src/Tools/expandshort	Thu Sep 26 17:30:52 1996 +0200
@@ -28,6 +28,7 @@
 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
+s/rtac *(\([a-zA-Z0-9_]*\)  *RS  *ssubst)  */stac \1 /g
 ' $f~~ | expand > $f
 done
 echo Finished.