
diff -r c1b5165b73db -r b60a9752b6d0 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Sat Oct 15 23:07:47 2016 +0200
+++ b/src/HOL/Num.thy	Sun Oct 16 09:31:03 2016 +0200
@@ -1217,7 +1217,7 @@
   K (
     Lin_Arith.add_simps
       @{thms arith_simps more_arith_simps rel_simps pred_numeral_simps
-        arith_special numeral_One of_nat_simps}
+        arith_special numeral_One of_nat_simps uminus_numeral_One}
     #> Lin_Arith.add_simps
       @{thms Suc_numeral Let_numeral Let_neg_numeral Let_0 Let_1
         le_Suc_numeral le_numeral_Suc less_Suc_numeral less_numeral_Suc




