--- a/src/FOL/IFOL.ML Wed Mar 26 18:51:57 1997 +0100
+++ b/src/FOL/IFOL.ML Thu Mar 27 10:06:36 1997 +0100
@@ -124,7 +124,7 @@
"[| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x)"
(fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]);
-(*Sometimes easier to use: the premises have no shared variables*)
+(*Sometimes easier to use: the premises have no shared variables. Safe!*)
qed_goal "ex_ex1I" IFOL.thy
"[| EX x.P(x); !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)"
(fn [ex,eq] => [ (rtac (ex RS exE) 1),