diff -r d27d79a47592 -r 3f309f885d0b src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Thu Jun 21 22:30:58 2007 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Thu Jun 21 22:52:22 2007 +0200
@@ -119,8 +119,8 @@
   addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
 val div_mod_ss = HOL_basic_ss addsimps simp_thms 
   @ map (symmetric o mk_meta_eq) 
-    [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, mod_add1_eq, 
-     mod_add_left_eq, mod_add_right_eq, 
+    [@{thm "dvd_eq_mod_eq_0"}, @{thm "zdvd_iff_zmod_eq_0"}, @{thm "mod_add1_eq"}, 
+     @{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, 
      @{thm "zmod_zadd1_eq"}, @{thm "zmod_zadd_left_eq"}, 
      @{thm "zmod_zadd_right_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}]
   @ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "DIVISION_BY_ZERO_MOD"},