src/HOL/Lifting_Set.thy

--- a/src/HOL/Lifting_Set.thy	Thu Apr 10 17:48:15 2014 +0200
+++ b/src/HOL/Lifting_Set.thy	Thu Apr 10 17:48:15 2014 +0200
@@ -45,9 +45,8 @@
   done
 
 lemma Domainp_set[relator_domain]:
-  assumes "Domainp T = R"
-  shows "Domainp (rel_set T) = (\<lambda>A. Ball A R)"
-using assms unfolding rel_set_def Domainp_iff[abs_def]
+  "Domainp (rel_set T) = (\<lambda>A. Ball A (Domainp T))"
+unfolding rel_set_def Domainp_iff[abs_def]
 apply (intro ext)
 apply (rule iffI) 
 apply blast