diff -r 0a51765d2084 -r cdf12a1cb963 src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Mon Feb 16 19:35:52 2009 -0800
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Feb 17 18:48:17 2009 +0100
@@ -34,7 +34,7 @@
 val nat_mod_add_eq = @{thm mod_add1_eq} RS sym;
 val nat_mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
 val nat_mod_add_right_eq = @{thm mod_add_right_eq} RS sym;
-val int_mod_add_eq = @{thm zmod_zadd1_eq} RS sym;
+val int_mod_add_eq = @{thm mod_add_eq} RS sym;
 val int_mod_add_left_eq = @{thm zmod_zadd_left_eq} RS sym;
 val int_mod_add_right_eq = @{thm zmod_zadd_right_eq} RS sym;
 val nat_div_add_eq = @{thm div_add1_eq} RS sym;