diff -r 30da58e0a483 -r aab5798e5a33 src/HOL/UNITY/Simple/Reach.thy
--- a/src/HOL/UNITY/Simple/Reach.thy	Thu Oct 04 21:11:06 2007 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Fri Oct 05 08:38:09 2007 +0200
@@ -121,7 +121,7 @@
 apply (unfold metric_def)
 apply (subgoal_tac "{v. ~ (s (x:=True)) v} = {v. ~ s v} - {x}")
  prefer 2 apply force
-apply (simp add: card_Suc_Diff1)
+apply (simp add: card_Suc_Diff1 del:card_Diff_insert)
 done
 
 lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s"