# HG changeset patch
# User huffman
# Date 1315067171 25200
# Node ID 49ef76b4a63491f2952f420e226225d10eb5e920
# Parent  761f427ef1ab3fa8b162508508a08167965c543f
remove duplicate lemma finite_choice in favor of finite_set_choice

diff -r 761f427ef1ab -r 49ef76b4a634 NEWS
--- a/NEWS	Sat Sep 03 09:12:19 2011 -0700
+++ b/NEWS	Sat Sep 03 09:26:11 2011 -0700
@@ -204,6 +204,7 @@
 removed, and other theorems have been renamed or replaced with more
 general versions. INCOMPATIBILITY.
 
+  finite_choice ~> finite_set_choice
   eventually_conjI ~> eventually_conj
   eventually_and ~> eventually_conj_iff
   eventually_false ~> eventually_False
diff -r 761f427ef1ab -r 49ef76b4a634 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sat Sep 03 09:12:19 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sat Sep 03 09:26:11 2011 -0700
@@ -270,13 +270,6 @@
 
 subsection {* Metric space *}
 
-(* TODO: move somewhere else *)
-lemma finite_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)"
-apply (induct set: finite, simp_all)
-apply (clarify, rename_tac y)
-apply (rule_tac x="f(x:=y)" in exI, simp)
-done
-
 instantiation vec :: (metric_space, finite) metric_space
 begin
 
@@ -311,7 +304,7 @@
       have "\<forall>i\<in>UNIV. \<exists>r>0. \<forall>y. dist y (x $ i) < r \<longrightarrow> y \<in> A i"
         using A unfolding open_dist by simp
       hence "\<exists>r. \<forall>i\<in>UNIV. 0 < r i \<and> (\<forall>y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i)"
-        by (rule finite_choice [OF finite])
+        by (rule finite_set_choice [OF finite])
       then obtain r where r1: "\<forall>i. 0 < r i"
         and r2: "\<forall>i y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i" by fast
       have "0 < Min (range r) \<and> (\<forall>y. dist y x < Min (range r) \<longrightarrow> y \<in> S)"