diff -r b22ecedde1c7 -r ae630bab13da src/HOL/Probability/Discrete_Topology.thy
--- a/src/HOL/Probability/Discrete_Topology.thy	Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy	Mon Jan 14 17:29:04 2013 +0100
@@ -48,7 +48,7 @@
   thus "\<exists>f::'a discrete \<Rightarrow> nat. inj f" by blast
 qed
 
-instance discrete :: (countable) countable_basis_space
+instance discrete :: (countable) second_countable_topology
 proof
   let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
   have "topological_basis ?B"