--- a/src/HOL/Tools/nat_numeral_simprocs.ML Tue Feb 09 11:07:14 2010 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Tue Feb 09 11:47:47 2010 +0100
@@ -124,7 +124,7 @@
(*Simplify 1*n and n*1 to n*)
-val add_0s = map rename_numerals [@{thm add_0}, @{thm Nat.add_0_right}];
+val add_0s = map rename_numerals [@{thm Nat.add_0}, @{thm Nat.add_0_right}];
val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
@@ -136,7 +136,7 @@
val simplify_meta_eq =
Arith_Data.simplify_meta_eq
- ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm Nat.add_0_right},
+ ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm Nat.add_0}, @{thm Nat.add_0_right},
@{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);