# HG changeset patch
# User nipkow
# Date 989589462 -7200
# Node ID 2d73013f3a4111adff6c384ff7f2c24630427f58
# Parent  38a69e5d79faecbd3f5e7a907847418f034f01d8
mult_Suc generally, not just for numerals.

diff -r 38a69e5d79fa -r 2d73013f3a41 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Fri May 11 13:49:15 2001 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML	Fri May 11 15:57:42 2001 +0200
@@ -574,10 +574,7 @@
    le_Suc_number_of,le_number_of_Suc,
    less_Suc_number_of,less_number_of_Suc,
    Suc_eq_number_of,eq_number_of_Suc,
-   read_instantiate_sg (sign_of(the_context()))
-      [("m","number_of ?v")] mult_Suc,
-   read_instantiate_sg (sign_of(the_context()))
-      [("m","number_of ?v")] mult_Suc_right,
+   mult_Suc, mult_Suc_right,
    eq_number_of_0, eq_0_number_of, less_0_number_of,
    nat_number_of, Let_number_of, if_True, if_False];