src/HOLCF/Up.thy

--- a/src/HOLCF/Up.thy	Thu Jan 17 00:51:20 2008 +0100
+++ b/src/HOLCF/Up.thy	Thu Jan 17 21:44:19 2008 +0100
@@ -117,7 +117,7 @@
 lemma up_lemma2:
   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom"
 apply (erule contrapos_nn)
-apply (drule_tac x="j" and y="i + j" in chain_mono3)
+apply (drule_tac i="j" and j="i + j" in chain_mono)
 apply (rule le_add2)
 apply (case_tac "Y j")
 apply assumption