src/HOL/HOL.ML

--- a/src/HOL/HOL.ML	Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/HOL.ML	Wed Jul 25 13:13:01 2001 +0200
@@ -12,7 +12,6 @@
   val refl = refl;
   val subst = subst;
   val ext = ext;
-  val someI = someI;
   val impI = impI;
   val mp = mp;
   val True_def = True_def;
@@ -31,6 +30,6 @@
 end;
 
 AddXIs [equal_intr_rule, disjI1, disjI2, ext];
-AddXEs [ex1_implies_ex, someI_ex, sym];
+AddXEs [ex1_implies_ex, sym];
 
 open HOL;