renamed Suc_card_Diff or something

--- a/src/HOL/UNITY/Reach.ML	Fri Oct 09 11:16:04 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Fri Oct 09 11:16:52 1998 +0200
@@ -91,7 +91,7 @@
 Goalw [metric_def] "~ s x ==> Suc (metric (s(x:=True))) = metric s";
 by (subgoal_tac "{v. ~ (s(x:=True)) v} = {v. ~ s v} - {x}" 1);
 by Auto_tac;
-by (asm_simp_tac (simpset() addsimps [card_Suc_Diff]) 1);
+by (asm_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1);
 qed "Suc_metric";
 
 Goal "~ s x ==> metric (s(x:=True)) < metric s";