--- a/src/HOL/Tools/nat_numeral_simprocs.ML Tue Nov 17 12:01:19 2015 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Tue Nov 17 12:32:08 2015 +0000
@@ -26,7 +26,7 @@
struct
(*Maps n to #n for n = 1, 2*)
-val numeral_syms = [@{thm numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
+val numeral_syms = [@{thm numeral_One} RS sym, @{thm numeral_2_eq_2} RS sym];
val numeral_sym_ss =
simpset_of (put_simpset HOL_basic_ss @{context} addsimps numeral_syms);
@@ -59,7 +59,7 @@
(** Other simproc items **)
val bin_simps =
- [@{thm numeral_1_eq_1} RS sym,
+ [@{thm numeral_One} RS sym,
@{thm numeral_plus_numeral}, @{thm add_numeral_left},
@{thm diff_nat_numeral}, @{thm diff_0_eq_0}, @{thm diff_0},
@{thm numeral_times_numeral}, @{thm mult_numeral_left(1)},