--- 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"