# HG changeset patch
# User paulson
# Date 843751852 -7200
# Node ID a3262b93c1d2eec6b9e7bbd76c5e5e5ed2694cd9
# Parent  6db93e6f1b1114bf51876d0b33b766d0524273ed
Now replaces uses of ssubst by stac

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.