src/HOL/Decision_Procs/mir_tac.ML

 val mod_div_equality' = @{thm "mod_div_equality'"};
 val split_div' = @{thm "split_div'"};
 val Suc_plus1 = @{thm "Suc_plus1"};
 val imp_le_cong = @{thm "imp_le_cong"};
 val conj_le_cong = @{thm "conj_le_cong"};
-val nat_mod_add_eq = @{thm "mod_add1_eq"} RS sym;
+val mod_add_eq = @{thm "mod_add_eq"} RS sym;
 val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
 val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
-val int_mod_add_eq = @{thm "mod_add_eq"} RS sym;
 val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
 val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
 val ZDIVISION_BY_ZERO_MOD = @{thm "DIVISION_BY_ZERO"} RS conjunct2;
 val ZDIVISION_BY_ZERO_DIV = @{thm "DIVISION_BY_ZERO"} RS conjunct1;
 

     val thy = ProofContext.theory_of ctxt
     (* Transform the term*)
     val (t,np,nh) = prepare_for_mir thy q g
     (* Some simpsets for dealing with mod div abs and nat*)
     val mod_div_simpset = HOL_basic_ss 
-                        addsimps [refl,nat_mod_add_eq, 
+                        addsimps [refl, mod_add_eq, 
                                   @{thm "mod_self"}, @{thm "zmod_self"},
                                   @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
                                   @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
                                   @{thm "Suc_plus1"}]
                         addsimps @{thms add_ac}