--- 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];