src/HOL/Probability/Independent_Family.thy

     assume "indep_vars M' X I"
     fix A assume "A \<in> sets P.P"
     moreover
     have "D.prob A = P.prob A"
     proof (rule prob_space_unique_Int_stable)
-      show "prob_space ?D'" by default
-      show "prob_space (Pi\<^isub>M I ?M)" by default
+      show "prob_space ?D'" by unfold_locales
+      show "prob_space (Pi\<^isub>M I ?M)" by unfold_locales
       show "Int_stable P.G" using M'.Int
         by (intro Int_stable_product_algebra_generator) (simp add: Int_stable_def)
       show "space P.G \<in> sets P.G"
         using M'.top by (simp add: product_algebra_generator_def)
       show "space ?D' = space P.G"  "sets ?D' = sets (sigma P.G)"

       by fact
     show "space ?P \<in> sets ?P"
       unfolding space_pair_measure[simplified pair_measure_def space_sigma]
       using X.top Y.top by (auto intro!: pair_measure_generatorI)
 
-    show "prob_space ?J" by default
+    show "prob_space ?J" by unfold_locales
     show "space ?J = space ?P"
       by (simp add: pair_measure_generator_def space_pair_measure)
     show "sets ?J = sets (sigma ?P)"
       by (simp add: pair_measure_def)
 
-    show "prob_space XY.P" by default
+    show "prob_space XY.P" by unfold_locales
     show "space XY.P = space ?P" "sets XY.P = sets (sigma ?P)"
       by (simp_all add: pair_measure_generator_def pair_measure_def)
 
     show "A \<in> sets (sigma ?P)"
       using `A \<in> sets P` unfolding P_def pair_measure_def by simp