--- a/src/HOL/Decision_Procs/mir_tac.ML Mon Feb 16 19:35:52 2009 -0800
+++ b/src/HOL/Decision_Procs/mir_tac.ML Tue Feb 17 18:48:17 2009 +0100
@@ -49,7 +49,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;