diff -r ded1c636aece -r de6cd60b1226 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Jun 07 23:23:48 2017 +0200
+++ b/src/HOL/Int.thy	Thu Jun 08 23:37:01 2017 +0200
@@ -1713,11 +1713,7 @@
   "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)"
   "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1"
   "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1"
-          apply (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
-        apply (simp_all only: algebra_simps minus_diff_eq)
-  apply (simp_all only: add.commute [of _ "- (numeral n + numeral n)"])
-  apply (simp_all only: minus_add add.assoc left_minus)
-  done
+  by (simp_all only: sub_def dup_def numeral.simps Pos_def Neg_def numeral_BitM)
 
 text \<open>Implementations.\<close>