src/HOLCF/IOA/meta_theory/SimCorrectness.ML

          corresp_ex_sim_def, Int_non_empty,Image_def]) 1);
   by (REPEAT (etac conjE 1));
   by (etac ballE 1);
   by (Blast_tac 2);
   by (etac exE 1);
-  by (rtac selectI2 1);
+  by (rtac someI2 1);
   by (assume_tac 1);
   by (Blast_tac 1);
 qed"simulation_starts";
 
 bind_thm("sim_starts1",(rewrite_rule [Let_def] simulation_starts) RS conjunct1);