# HG changeset patch
# User paulson
# Date 859453596 -3600
# Node ID ea49c12f677fc57745887a99f3c5a5dde5471d85
# Parent  143ebf752e78cf35cf8d7cf6f4eda982b9d07e9f
Updated comment

diff -r 143ebf752e78 -r ea49c12f677f src/FOL/IFOL.ML
--- 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),