src/HOL/Induct/Exp.ML

--- a/src/HOL/Induct/Exp.ML	Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Induct/Exp.ML	Wed Dec 24 10:02:30 1997 +0100
@@ -109,7 +109,7 @@
 (*This theorem says that "WHILE TRUE DO c" cannot terminate*)
 goal thy "!!x. (c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
 by (etac exec.induct 1);
-by (Auto_tac());
+by Auto_tac;
 bind_thm ("while_true_E", refl RSN (2, result() RS mp));