src/HOL/Probability/Complete_Measure.thy

   "completion M = measure_of (space M) { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }
     (emeasure M \<circ> main_part M)"
 
 lemma completion_into_space:
   "{ S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } \<subseteq> Pow (space M)"
-  using sets_into_space by auto
+  using sets.sets_into_space by auto
 
 lemma space_completion[simp]: "space (completion M) = space M"
   unfolding completion_def using space_measure_of[OF completion_into_space] by simp
 
 lemma completionI:

   "sigma_algebra (space M) { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
     (is "sigma_algebra _ ?A")
   unfolding sigma_algebra_iff2
 proof (intro conjI ballI allI impI)
   show "?A \<subseteq> Pow (space M)"
-    using sets_into_space by auto
+    using sets.sets_into_space by auto
 next
   show "{} \<in> ?A" by auto
 next
   let ?C = "space M"
   fix A assume "A \<in> ?A" from completionE[OF this] guess S N N' .

     fix x assume "x \<in> space M"
     have "?f' -` {?f' x} \<inter> space M =
       (if x \<in> ?N then ?F undefined \<union> ?N
        else if f x = undefined then ?F (f x) \<union> ?N
        else ?F (f x) - ?N)"
-      using N(2) sets_into_space by (auto split: split_if_asm simp: null_sets_def)
+      using N(2) sets.sets_into_space by (auto split: split_if_asm simp: null_sets_def)
     moreover { fix y have "?F y \<union> ?N \<in> sets M"
       proof cases
         assume y: "y \<in> f`space M"
         have "?F y \<union> ?N = (main_part M (?F y) \<union> null_part M (?F y)) \<union> ?N"
           using main_part_null_part_Un[OF F] by auto