diff -r fb0fb0209c87 -r 46f128d8133c src/ZF/Integ/Bin.ML
--- a/src/ZF/Integ/Bin.ML	Sun Nov 11 21:38:54 2001 +0100
+++ b/src/ZF/Integ/Bin.ML	Mon Nov 12 10:37:36 2001 +0100
@@ -348,7 +348,7 @@
 by (ALLGOALS (asm_full_simp_tac 
 	      (simpset() addsimps zcompare_rls @ 
 			  [zminus_zadd_distrib RS sym, int_of_add RS sym])));
-by (subgoal_tac "znegative ($- $# succ(x)) <-> znegative ($# succ(x))" 1);
+by (subgoal_tac "znegative ($- $# succ(n)) <-> znegative ($# succ(n))" 1);
 by (Asm_simp_tac 2);
 by (Full_simp_tac 1);
 qed "iszero_integ_of_BIT"; 
@@ -391,7 +391,7 @@
 by (ALLGOALS (asm_full_simp_tac 
 	      (simpset() addsimps [zminus_zadd_distrib RS sym, zdiff_def,
 				   int_of_add RS sym])));
-by (subgoal_tac "$#1 $- $# succ(succ(x #+ x)) = $- $# succ(x #+ x)" 1);
+by (subgoal_tac "$#1 $- $# succ(succ(n #+ n)) = $- $# succ(n #+ n)" 1);
 by (asm_full_simp_tac (simpset() addsimps [zdiff_def])1);
 by (asm_simp_tac (simpset() addsimps [equation_zminus, int_of_diff RS sym])1);
 qed "neg_integ_of_BIT";