src/HOL/Hilbert_Choice_lemmas.ML

--- a/src/HOL/Hilbert_Choice_lemmas.ML	Wed Dec 05 03:06:05 2001 +0100
+++ b/src/HOL/Hilbert_Choice_lemmas.ML	Wed Dec 05 03:07:44 2001 +0100
@@ -17,7 +17,6 @@
 by (etac exE 1);
 by (etac someI 1);
 qed "someI_ex";
-AddXEs [someI_ex];
 
 (*Easier to apply than someI: conclusion has only one occurrence of P*)
 val prems = Goal "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";