src/HOL/HOLCF/Lift.thy

--- a/src/HOL/HOLCF/Lift.thy	Tue Nov 30 15:34:51 2010 -0800
+++ b/src/HOL/HOLCF/Lift.thy	Tue Nov 30 15:56:19 2010 -0800
@@ -87,7 +87,7 @@
 
 lemma cont2cont_lift_case [simp]:
   "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case \<bottom> (f x) (g x))"
-unfolding lift_case_eq by (simp add: cont_Rep_lift [THEN cont_compose])
+unfolding lift_case_eq by (simp add: cont_Rep_lift)
 
 subsection {* Further operations *}