no_qed;

--- a/src/HOL/Induct/Acc.ML	Fri Sep 03 14:52:19 1999 +0200
+++ b/src/HOL/Induct/Acc.ML	Fri Sep 03 14:53:55 1999 +0200
@@ -27,6 +27,8 @@
 by (Blast_tac 1);
  by (blast_tac (claset() addDs [acc_downward]) 1);
 val lemma = result();
+no_qed();
+
 Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r";
 by (blast_tac (claset() addDs [lemma]) 1);
 qed "acc_downwards";