diff -r 09974789e483 -r 773b378d9313 src/HOL/Library/Nat_Bijection.thy
--- a/src/HOL/Library/Nat_Bijection.thy	Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Library/Nat_Bijection.thy	Thu Oct 30 21:02:01 2014 +0100
@@ -122,7 +122,7 @@
 by (induct x) simp_all
 
 lemma sum_decode_inverse [simp]: "sum_encode (sum_decode n) = n"
-  by (simp add: even_two_times_div_two odd_two_times_div_two_Suc sum_decode_def sum_encode_def)
+  by (simp add: even_two_times_div_two sum_decode_def sum_encode_def)
 
 lemma inj_sum_encode: "inj_on sum_encode A"
 by (rule inj_on_inverseI, rule sum_encode_inverse)
@@ -269,12 +269,18 @@
 by auto
 
 lemma div2_even_ext_nat:
-  "x div 2 = y div 2 \<Longrightarrow> even x \<longleftrightarrow> even y \<Longrightarrow> (x::nat) = y"
-apply (rule mod_div_equality [of x 2, THEN subst])
-apply (rule mod_div_equality [of y 2, THEN subst])
-apply (cases "even x")
-apply (simp_all add: even_iff_mod_2_eq_zero)
-done
+  fixes x y :: nat
+  assumes "x div 2 = y div 2"
+  and "even x \<longleftrightarrow> even y"
+  shows "x = y"
+proof -
+  from `even x \<longleftrightarrow> even y` have "x mod 2 = y mod 2"
+    by (simp only: even_iff_mod_2_eq_zero) auto
+  with assms have "x div 2 * 2 + x mod 2 = y div 2 * 2 + y mod 2"
+    by simp
+  then show ?thesis
+    by simp
+qed
 
 
 subsubsection {* From sets to naturals *}