diff -r 7759f1766189 -r 50c715579715 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 17 15:22:14 2016 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Dec 17 15:22:14 2016 +0100
@@ -45,8 +45,8 @@
     (* Some simpsets for dealing with mod div abs and nat*)
     val mod_div_simpset =
       put_simpset HOL_basic_ss ctxt
-      addsimps @{thms refl mod_add_eq [symmetric] mod_add_left_eq [symmetric]
-          mod_add_right_eq [symmetric]
+      addsimps @{thms refl mod_add_eq mod_add_left_eq
+          mod_add_right_eq
           div_add1_eq [symmetric] zdiv_zadd1_eq [symmetric]
           mod_self
           div_by_0 mod_by_0 div_0 mod_0