int_Suc->int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc

--- a/src/HOL/Integ/Int.ML	Mon May 24 15:54:12 1999 +0200
+++ b/src/HOL/Integ/Int.ML	Mon May 24 15:54:58 1999 +0200
@@ -24,12 +24,12 @@
 Goal "(w < z + int (Suc m)) = (w < z + int m | w = z + int m)";
 by (auto_tac (claset(),
 	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, zadd_int]));
-by (cut_inst_tac [("m","m")] int_Suc 1);
-by (cut_inst_tac [("m","n")] int_Suc 1);
+by (cut_inst_tac [("m","m")] int_Suc_int_1 1);
+by (cut_inst_tac [("m","n")] int_Suc_int_1 1);
 by (Asm_full_simp_tac 1);
 by (exhaust_tac "n" 1);
 by Auto_tac;
-by (cut_inst_tac [("m","m")] int_Suc 1);
+by (cut_inst_tac [("m","m")] int_Suc_int_1 1);
 by (full_simp_tac (simpset() addsimps zadd_ac) 1);
 by (asm_full_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
 by (auto_tac (claset(),

--- a/src/HOL/Integ/IntDef.ML	Mon May 24 15:54:12 1999 +0200
+++ b/src/HOL/Integ/IntDef.ML	Mon May 24 15:54:58 1999 +0200
@@ -220,7 +220,7 @@
 
 Goal "int (Suc m) = int 1 + (int m)";
 by (simp_tac (simpset() addsimps [zadd_int]) 1);
-qed "int_Suc";
+qed "int_Suc_int_1";
 
 Goalw [int_def] "int 0 + z = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);