# HG changeset patch
# User wenzelm
# Date 901875811 -7200
# Node ID 66925577cefe2a6e8c6c2d9cf3d1dde1eff6b014
# Parent  e5a6ace920a0fff2e88200771f0428c1536c8eb0
isatool expandshort;

diff -r e5a6ace920a0 -r 66925577cefe src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Fri Jul 31 11:03:21 1998 +0200
+++ b/src/HOL/HOL.ML	Fri Jul 31 11:03:31 1998 +0200
@@ -251,9 +251,9 @@
   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
 
 Goal "?! x. P x ==> ? x. P x";
-be ex1E 1;
-br exI 1;
-ba 1;
+by (etac ex1E 1);
+by (rtac exI 1);
+by (assume_tac 1);
 qed "ex1_implies_ex";