--- 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)"