1.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -546,10 +546,10 @@
     1.4  lemma split_paired_Eps: "(SOME x. P x) = (SOME (a,b). P(a,b))"
     1.5    by simp
     1.6  
     1.7 -lemma Eps_split: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
     1.8 +lemma Eps_case_prod: "Eps (case_prod P) = (SOME xy. P (fst xy) (snd xy))"
     1.9    by (simp add: split_def)
    1.10  
    1.11 -lemma Eps_split_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
    1.12 +lemma Eps_case_prod_eq [simp]: "(@(x',y'). x = x' & y = y') = (x,y)"
    1.13    by blast
    1.14  
    1.15