src/HOL/Library/Word.thy

     hence orig: "(2 * bv_to_nat w + 1) mod 2 = 2 * q mod 2" (is "?lhs = ?rhs")
       by simp
     have "?lhs = (1 + 2 * bv_to_nat w) mod 2"
       by (simp add: add_commute)
     also have "... = 1"
-      by (subst mod_add1_eq) simp
+      by (subst mod_add_eq) simp
     finally have eq1: "?lhs = 1" .
     have "?rhs  = 0" by simp
     with orig and eq1
     show "nat_to_bv (Suc (2 * bv_to_nat w) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])"
       by simp