src/ZF/Resid/Reduction.thy

--- a/src/ZF/Resid/Reduction.thy	Mon Sep 30 16:47:03 2002 +0200
+++ b/src/ZF/Resid/Reduction.thy	Mon Sep 30 16:48:15 2002 +0200
@@ -236,8 +236,6 @@
      "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)"
 apply (erule Scomp.induct)
 apply (auto simp add: unmmark_subst_rec)
-apply (drule_tac psi = "Fun (?u) =1=> ?w" in asm_rl)
-apply auto
 done
 
 lemma completeness: "[|u \<in> lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)"