diff -r 54dbe0368dc6 -r e46acc0ea1fe src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Thu Aug 26 15:20:41 2010 +0200
+++ b/src/HOL/Probability/Borel.thy	Thu Aug 26 18:41:54 2010 +0200
@@ -81,7 +81,7 @@
   "(\<lambda>x. c) \<in> borel_measurable M"
   by (auto intro!: measurable_const)
 
-lemma (in sigma_algebra) borel_measurable_indicator:
+lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]:
   assumes A: "A \<in> sets M"
   shows "indicator A \<in> borel_measurable M"
   unfolding indicator_def_raw using A