diff -r f6b9f528c89c -r 6571c78c9667 src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Tue Nov 17 12:01:19 2015 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML	Tue Nov 17 12:32:08 2015 +0000
@@ -122,7 +122,7 @@
       (case Rat.quotient_of_rat x of (i, 1) => i | _ => error "int_of_rat: bad int")),
     conv = (fn ctxt =>
       Simplifier.rewrite (put_simpset semiring_norm_ss ctxt)
-      then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_1_eq_1}))};
+      then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_One}))};
 
 val divide_const = Thm.cterm_of @{context} (Logic.varify_global @{term "op /"});
 val [divide_tvar] = Term.add_tvars (Thm.term_of divide_const) [];
@@ -257,10 +257,10 @@
 val is_number = can dest_number;
 
 fun numeral01_conv ctxt =
-  Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_1_eq_1}]);
+  Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_One}]);
 
 fun zero1_numeral_conv ctxt =
-  Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_1_eq_1} RS sym]);
+  Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_One} RS sym]);
 
 fun zerone_conv ctxt cv =
   zero1_numeral_conv ctxt then_conv cv then_conv numeral01_conv ctxt;