--- a/src/HOLCF/Lift.thy Thu Apr 13 23:14:18 2006 +0200
+++ b/src/HOLCF/Lift.thy Thu Apr 13 23:15:44 2006 +0200
@@ -84,7 +84,7 @@
lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y = (Def x = y)"
apply (induct y)
-apply (simp add: eq_UU_iff)
+apply simp
apply (simp add: Def_inject_less_eq)
done