src/HOL/Real/Hyperreal/Zorn.ML

--- a/src/HOL/Real/Hyperreal/Zorn.ML	Fri Sep 15 11:34:46 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.ML	Fri Sep 15 12:39:57 2000 +0200
@@ -32,7 +32,7 @@
 by (auto_tac (claset(),simpset() addsimps [super_def,
                maxchain_def,psubset_def]));
 by (rtac swap 1 THEN assume_tac 1);
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by (ALLGOALS(Blast_tac));
 qed "Abrial_axiom1";
 
@@ -167,7 +167,7 @@
 Goal "c: chain S - maxchain S ==> \
 \                         (@c'. c': super S c): super S c";
 by (etac (mem_super_Ex RS exE) 1);
-by (rtac selectI2 1);
+by (rtac someI2 1);
 by (Auto_tac);
 qed "select_super";