--- a/src/HOL/Hilbert_Choice.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Hilbert_Choice.thy Tue Oct 13 09:21:15 2015 +0200
@@ -546,10 +546,10 @@
lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
by simp
-lemma Eps_split: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
+lemma Eps_case_prod: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
by (simp add: split_def)
-lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
+lemma Eps_case_prod_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
by blast