src/HOL/Probability/Borel.thy

         by (metis surj_def)
       obtain n where n: "prod_decode n = (i,j)" using surj_prod_decode
         by (metis surj_def)
 
       from Fract i j n show ?thesis
-        by (metis prod.cases prod_case_split)
+        by (metis prod.cases)
   qed
 qed
 
 lemma rats_enumeration: "\<rat> = range (of_rat o nat_to_rat_surj)" 
   using nat_to_rat_surj