# HG changeset patch
# User wenzelm
# Date 995658807 -7200
# Node ID cf7dae62d69d032f2c5e0e5a1fb8492403291798
# Parent  8a203ae6efe39ab4ad7d6bc26c9c9e6d9b150ae3
tuned;

diff -r 8a203ae6efe3 -r cf7dae62d69d src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Fri Jul 20 21:52:54 2001 +0200
+++ b/src/HOL/HOL_lemmas.ML	Fri Jul 20 21:53:27 2001 +0200
@@ -421,7 +421,7 @@
 by (REPEAT (ares_tac [prema,premx] 1));
 qed "theI";
 
-Goal "(EX! x. P x) ==> P (THE x. P x)";
+Goal "EX! x. P x ==> P (THE x. P x)";
 by (etac ex1E 1);
 by (etac theI 1);
 by (etac allE 1);