# HG changeset patch
# User oheimb
# Date 980876820 -3600
# Node ID 498d0db8cd8a8ce227ba5b0d72713647509452d3
# Parent  b044cf3500a25903bd8fc77832a0af956ef55274
removed (obsolete) mult_assumption

diff -r b044cf3500a2 -r 498d0db8cd8a lib/scripts/convert.pl
--- a/lib/scripts/convert.pl	Tue Jan 30 14:48:27 2001 +0100
+++ b/lib/scripts/convert.pl	Tue Jan 30 18:47:00 2001 +0100
@@ -17,13 +17,6 @@
   $s;
 }
 
-sub mult_assumption {
-  my $n = shift;
-  my $r = "";
-  for($i=0; $i<$n; $i++) { $r = $r.", assumption"; }
-  $r;
-}
-
 sub process_tac {
   my $lead = shift;
   my $t = shift;
@@ -100,20 +93,19 @@
   s/rtac ([\w\.]+) 1/rule $1/g;
   s/rtac ([\w\.]+) (\d+)/rule_tac [$2] $1/g;
   s/res_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/rule_tac $1 = $2 $3/g;
-  s/ratac ([\w\.]+) (\d+) 1/"rule $1".mult_assumption($2)/eg;
   s/dtac ([\w\.]+) 1/drule $1/g;
   s/dtac ([\w\.]+) (\d+)/drule_tac [$2] $1/g;
   s/dres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/drule_tac $1 = $2 $3/g;
-  s/datac ([\w\.]+) (\d+) 1/"drule $1".mult_assumption($2)/eg;
+  s/datac ([\w\.]+) (\d+) 1/"drule ($2) $1"/g;
   s/etac ([\w\.]+) 1/erule $1/g;
   s/etac ([\w\.]+) (\d+)/erule_tac [$2] $1/g;
   s/eres_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/erule_tac $1 = $2 $3/g;
-  s/eatac ([\w\.]+) (\d+) 1/"erule $1".mult_assumption($2)/eg;
+  s/eatac ([\w\.]+) (\d+) 1/"erule ($2) $1"/g;
   s/forward_tac \[([\w\.]+)\] 1/frule $1/g;
   s/ftac ([\w\.]+) 1/frule $1/g;
   s/ftac ([\w\.]+) (\d+)/frule_tac [$2] $1/g;
   s/forw_inst_tac \[\((\".*?\"),(\".*?\")\)\] ([\w\.]+) 1/frule_tac $1 = $2 $3/g;
-  s/fatac ([\w\.]+) (\d+) 1/"frule $1".mult_assumption($2)/eg;
+  s/fatac ([\w\.]+) (\d+) 1/"frule ($2) $1"/g;
 
 
   s/THEN /, /g;