# HG changeset patch
# User wenzelm
# Date 938803318 -7200
# Node ID 4434adbe24a1887e6fab0c3e572e380c2dbba5d8
# Parent  27bbbe36d49ac3b004e8968b91289fa305a2eafe
fixed no_qed;

diff -r 27bbbe36d49a -r 4434adbe24a1 src/HOL/Induct/Acc.ML
--- 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);