diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -2096,7 +2096,7 @@
 lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M"
   using sets.sets_into_space unfolding restrict_space_def by (subst space_measure_of) auto
 
-lemma space_restrict_space2: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
+lemma space_restrict_space2 [simp]: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
   by (simp add: space_restrict_space sets.sets_into_space)
 
 lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = ((\<inter>) \<Omega>) ` sets M"