src/HOL/Probability/Regularity.thy

--- a/src/HOL/Probability/Regularity.thy	Mon Jan 14 17:16:59 2013 +0100
+++ b/src/HOL/Probability/Regularity.thy	Mon Jan 14 17:29:04 2013 +0100
@@ -104,7 +104,7 @@
 qed
 
 lemma
-  fixes M::"'a::{countable_basis_space, complete_space} measure"
+  fixes M::"'a::{second_countable_topology, complete_space} measure"
   assumes sb: "sets M = sets borel"
   assumes "emeasure M (space M) \<noteq> \<infinity>"
   assumes "B \<in> sets borel"