src/HOL/HOL.ML

   val if_def = if_def;
   val arbitrary_def = arbitrary_def;
 end;
 
 AddXIs [equal_intr_rule, disjI1, disjI2, ext];
-AddXEs [ex1_implies_ex];
+AddXEs [ex1_implies_ex, someI_ex];
 
 open HOL;