src/HOL/Probability/Caratheodory.thy

       fix x i
       assume x: "x \<in> A i"
       with sbBB [of i] obtain j where "x \<in> BB i j"
         by blast
       thus "\<exists>i. x \<in> split BB (prod_decode i)"
-        by (metis prod_encode_inverse prod.cases)
+        by (metis prod_encode_inverse prod.case)
     qed
     have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
       by (rule ext)  (auto simp add: C_def)
     moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
       using BB posf[unfolded positive_def]