--- a/src/HOLCF/Cfun.thy Fri May 27 00:15:24 2005 +0200
+++ b/src/HOLCF/Cfun.thy Fri May 27 00:16:18 2005 +0200
@@ -632,7 +632,7 @@
apply (rule contlubI [rule_format])
apply (case_tac "x = \<bottom>")
apply (simp add: Istrictify1)
-apply (simp add: lub_const [THEN thelubI])
+apply (simp add: thelub_const)
apply (simp add: Istrictify2)
apply (erule contlub_cfun_fun)
done
@@ -641,7 +641,7 @@
apply (rule contlubI [rule_format])
apply (case_tac "lub (range Y) = \<bottom>")
apply (simp add: Istrictify1 chain_UU_I)
-apply (simp add: lub_const [THEN thelubI])
+apply (simp add: thelub_const)
apply (simp add: Istrictify2)
apply (simp add: contlub_cfun_arg)
apply (rule lub_equal2)