src/HOL/Integ/nat_simprocs.ML

    add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
    eq_nat_number_of, less_nat_number_of, le_number_of_eq_not_less,
    le_Suc_number_of,le_number_of_Suc,
    less_Suc_number_of,less_number_of_Suc,
    Suc_eq_number_of,eq_number_of_Suc,
-   mult_0, mult_0_right, mult_Suc, mult_Suc_right,
+   mult_Suc, mult_Suc_right,
    eq_number_of_0, eq_0_number_of, less_0_number_of,
-   nat_number_of, thm "Let_number_of", if_True, if_False];
+   nat_number_of, if_True, if_False];
 
 val simprocs = [Nat_Times_Assoc.conv,
                 Nat_Numeral_Simprocs.combine_numerals]@
                 Nat_Numeral_Simprocs.cancel_numerals;