--- a/src/HOL/Hilbert_Choice.thy Tue Oct 05 10:30:50 2010 +0200
+++ b/src/HOL/Hilbert_Choice.thy Tue Oct 05 10:59:12 2010 +0200
@@ -80,7 +80,7 @@
subsection{*Axiom of Choice, Proved Using the Description Operator*}
-lemma choice [meson_choice]: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
+lemma choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
by (fast elim: someI)
lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"