src/HOL/Probability/Fin_Map.thy
changeset 50094 84ddcf5364b4
parent 50091 b3b5dc2350b7
child 50100 9af8721ecd20
--- a/src/HOL/Probability/Fin_Map.thy	Thu Nov 15 17:40:46 2012 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Fri Nov 16 11:22:22 2012 +0100
@@ -500,7 +500,7 @@
   "topological_basis (range (enum_basis_finmap))"
 proof (subst topological_basis_iff, safe)
   fix n::nat
-  show "open (enum_basis_finmap n::('a \<Rightarrow>\<^isub>F 'b) set)" using enumerable_basis
+  show "open (enum_basis_finmap n::('a \<Rightarrow>\<^isub>F 'b) set)" using enum_basis_basis
     by (auto intro!: open_Pi'I simp: topological_basis_def enum_basis_finmap_def Let_def)
 next
   fix O'::"('a \<Rightarrow>\<^isub>F 'b) set" and x
@@ -514,7 +514,7 @@
     fix i assume "i \<in> domain x"
     have "open (ball (x i) e')" "x i \<in> ball (x i) e'" using e
       by (auto simp add: e'_def intro!: divide_pos_pos)
-    from enumerable_basisE[OF this] guess b' .
+    from topological_basisE[OF enum_basis_basis this] guess b' .
     thus "\<exists>y. x i \<in> enum_basis y \<and>
             enum_basis y \<subseteq> ball (x i) e'" by auto
   qed