--- a/src/HOL/Probability/Projective_Limit.thy Mon Jan 14 17:53:37 2013 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy Mon Jan 14 18:30:36 2013 +0100
@@ -46,12 +46,13 @@
end
lemma compactE':
+ fixes S :: "'a :: metric_space set"
assumes "compact S" "\<forall>n\<ge>m. f n \<in> S"
obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) ---> l) sequentially"
proof atomize_elim
have "subseq (op + m)" by (simp add: subseq_def)
have "\<forall>n. (f o (\<lambda>i. m + i)) n \<in> S" using assms by auto
- from compactE[OF `compact S` this] guess l r .
+ from seq_compactE[OF `compact S`[unfolded compact_eq_seq_compact_metric] this] guess l r .
hence "l \<in> S" "subseq ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) ----> l"
using subseq_o[OF `subseq (op + m)` `subseq r`] by (auto simp: o_def)
thus "\<exists>l r. l \<in> S \<and> subseq r \<and> (f \<circ> r) ----> l" by blast