diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Bali/Basis.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -16,7 +16,7 @@
 declare if_weak_cong [cong del] option.case_cong_weak [cong del]
 declare length_Suc_conv [iff]
 
-lemma Collect_split_eq: "{p. P (split f p)} = {(a,b). P (f a b)}"
+lemma Collect_split_eq: "{p. P (case_prod f p)} = {(a,b). P (f a b)}"
   by auto
 
 lemma subset_insertD: "A \<subseteq> insert x B \<Longrightarrow> A \<subseteq> B \<and> x \<notin> A \<or> (\<exists>B'. A = insert x B' \<and> B' \<subseteq> B)"