src/HOL/Fun.ML

--- a/src/HOL/Fun.ML	Tue Sep 05 10:12:48 2000 +0200
+++ b/src/HOL/Fun.ML	Tue Sep 05 10:13:20 2000 +0200
@@ -21,9 +21,7 @@
 
 (** "Axiom" of Choice, proved using the description operator **)
 
-Goal "!!Q. ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
-by (fast_tac (claset() addEs [selectI]) 1);
-qed "choice";
+(*"choice" is now proved in Tools/meson.ML*)
 
 Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
 by (fast_tac (claset() addEs [selectI]) 1);