src/HOLCF/Cprod.thy

--- a/src/HOLCF/Cprod.thy	Fri May 27 00:15:24 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Fri May 27 00:16:18 2005 +0200
@@ -138,14 +138,14 @@
 apply (rule contlubI [rule_format])
 apply (subst thelub_cprod)
 apply (erule monofun_pair1 [THEN ch2ch_monofun])
-apply (simp add: lub_const [THEN thelubI])
+apply (simp add: thelub_const)
 done
 
 lemma contlub_pair2: "contlub (\<lambda>y. (x, y))"
 apply (rule contlubI [rule_format])
 apply (subst thelub_cprod)
 apply (erule monofun_pair2 [THEN ch2ch_monofun])
-apply (simp add: lub_const [THEN thelubI])
+apply (simp add: thelub_const)
 done
 
 lemma cont_pair1: "cont (\<lambda>x. (x, y))"