diff -r 10e033194e9d -r adafef6eb295 src/HOL/Induct/Acc.ML
--- a/src/HOL/Induct/Acc.ML	Tue Jul 21 08:54:09 1998 +0200
+++ b/src/HOL/Induct/Acc.ML	Tue Jul 21 12:12:52 1998 +0200
@@ -25,12 +25,12 @@
 qed "acc_downward";
 
 Goal "(b,a) : r^* ==> a : acc r --> b : acc r";
-be rtrancl_induct 1;
-by(Blast_tac 1);
- by(blast_tac (claset() addDs [acc_downward]) 1);
+by (etac rtrancl_induct 1);
+by (Blast_tac 1);
+ by (blast_tac (claset() addDs [acc_downward]) 1);
 val lemma = result();
 Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r";
-by(blast_tac (claset() addDs [lemma]) 1);
+by (blast_tac (claset() addDs [lemma]) 1);
 qed "acc_downwards";
 
 val [major,indhyp] = goal Acc.thy