--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Sep 15 12:39:57 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Sep 15 15:30:50 2000 +0200
@@ -86,11 +86,11 @@
(* Go on as usual *)
by (etac exE 1);
by (dres_inst_tac [("x","t'"),
- ("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] selectI 1);
+ ("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] someI 1);
by (etac exE 1);
by (etac conjE 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def]) 1);
-by (res_inst_tac [("x","ex")] selectI 1);
+by (res_inst_tac [("x","ex")] someI 1);
by (etac conjE 1);
by (assume_tac 1);
qed"move_is_move_sim";