src/HOL/Relation.ML

--- a/src/HOL/Relation.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Relation.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -442,12 +442,12 @@
 by (rtac CollectI 1);
 by (rtac allI 1);
 by (etac allE 1);
-by (rtac (select_eq_Ex RS iffD2) 1);
+by (rtac (some_eq_ex RS iffD2) 1);
 by (etac ex1_implies_ex 1);
 by (rtac ext 1);
 by (etac CollectE 1);
 by (REPEAT (etac allE 1));
-by (rtac (select1_equality RS sym) 1);
+by (rtac (some1_equality RS sym) 1);
 by (atac 1);
 by (atac 1);
 qed "fun_rel_comp_unique";