# HG changeset patch
# User nipkow
# Date 907924612 -7200
# Node ID 9baad17accb9eecf099076e0f2f8ef19f3a5fa6e
# Parent  15b7f12ad91903d5a79abf237b5465f359968bdd
renamed Suc_card_Diff or something

diff -r 15b7f12ad919 -r 9baad17accb9 src/HOL/UNITY/Reach.ML
--- 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";