diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Hilbert_Choice.thy
--- 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