# HG changeset patch
# User paulson
# Date 886420091 -3600
# Node ID ff0c5c57fdfbd33253919a210923aa6c81e62006
# Parent  f88e466c43fa08aaf42cabfa970e283b84a045d0
Replaced \\1 by $1 as Perl itself asked me to...

diff -r f88e466c43fa -r ff0c5c57fdfb lib/scripts/expandshort.pl
--- a/lib/scripts/expandshort.pl	Fri Jan 30 12:31:59 1998 +0100
+++ b/lib/scripts/expandshort.pl	Mon Feb 02 12:48:11 1998 +0100
@@ -16,24 +16,24 @@
     $_ = $text;
 
     s/\bsafe_tac *\(claset *\( *\) *\)/Safe_tac/sg;
-    s/ *\(Safe_tac\) *([0-9]+)/ Safe_tac \1/sg;
+    s/ *\(Safe_tac\) *([0-9]+)/ Safe_tac $1/sg;
     s/ *\(Safe_tac\)/ Safe_tac/sg;
     s/\bby\(/by (/sg;
-    s/\bba\b *(\d+);/by (assume_tac \1);/sg;
-    s/\bbr\b *([^;.*!]*) (\d+);/by (rtac \1 \2);/sg;
-    s/\bbrs\b *([^;.*!]*) (\d+);/by (resolve_tac \1 \2);/sg;
-    s/\bbd\b *([^;.*!]*) (\d+);/by (dtac \1 \2);/sg;
-    s/\bbds\b *([^;.*!]*) (\d+);/by (dresolve_tac \1 \2);/sg;
-    s/\bbe\b *([^;.*!]*) (\d+);/by (etac \1 \2);/sg;
-    s/\bbes\b *([^;.*!]*) (\d+);/by (eresolve_tac \1 \2);/sg;
-    s/\bbw\b *([^;.*!]*);/by (rewtac \1);/sg;
-    s/\bbws\b *([^;.*!]*);/by (rewrite_goals_tac \1);/sg;
+    s/\bba\b *(\d+);/by (assume_tac $1);/sg;
+    s/\bbr\b *([^;.*!]*) (\d+);/by (rtac $1 $2);/sg;
+    s/\bbrs\b *([^;.*!]*) (\d+);/by (resolve_tac $1 $2);/sg;
+    s/\bbd\b *([^;.*!]*) (\d+);/by (dtac $1 $2);/sg;
+    s/\bbds\b *([^;.*!]*) (\d+);/by (dresolve_tac $1 $2);/sg;
+    s/\bbe\b *([^;.*!]*) (\d+);/by (etac $1 $2);/sg;
+    s/\bbes\b *([^;.*!]*) (\d+);/by (eresolve_tac $1 $2);/sg;
+    s/\bbw\b *([^;.*!]*);/by (rewtac $1);/sg;
+    s/\bbws\b *([^;.*!]*);/by (rewrite_goals_tac $1);/sg;
     s/\bauto *\(\)/by Auto_tac/sg;
-    s/dresolve_tac *\[(\w+)\] */dtac \1 /sg;
-    s/eresolve_tac *\[(\w+)\] */etac \1 /sg;
-    s/resolve_tac *\[(\w+)\] */rtac \1 /sg;
-    s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac \1\2/sg;
-    s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac \1 /sg;
+    s/dresolve_tac *\[(\w+)\] */dtac $1 /sg;
+    s/eresolve_tac *\[(\w+)\] */etac $1 /sg;
+    s/resolve_tac *\[(\w+)\] */rtac $1 /sg;
+    s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac $1$2/sg;
+    s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac $1 /sg;
 
     $result = $_;