fixed no_qed;

--- a/src/HOL/Induct/Acc.ML	Fri Oct 01 20:40:03 1999 +0200
+++ b/src/HOL/Induct/Acc.ML	Fri Oct 01 20:41:58 1999 +0200
@@ -26,8 +26,8 @@
 by (etac rtrancl_induct 1);
 by (Blast_tac 1);
  by (blast_tac (claset() addDs [acc_downward]) 1);
+no_qed();
 val lemma = result();
-no_qed();
 
 Goal "[| a : acc r; (b,a) : r^* |] ==> b : acc r";
 by (blast_tac (claset() addDs [lemma]) 1);