--- a/src/HOL/UNITY/SubstAx.thy Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/UNITY/SubstAx.thy Mon Jun 05 14:22:58 2006 +0200
@@ -363,7 +363,7 @@
==> F \<in> A LeadsTo ((A \<inter> (f-`(atLeast l))) \<union> B)"
apply (rule_tac f = f and f1 = "%k. l - k"
in wf_less_than [THEN wf_inv_image, THEN LeadsTo_wf_induct])
-apply (simp add: inv_image_def Image_singleton, clarify)
+apply (simp add: Image_singleton, clarify)
apply (case_tac "m<l")
apply (blast intro: LeadsTo_weaken_R diff_less_mono2)
apply (blast intro: not_leE subset_imp_LeadsTo)