src/HOL/Relation.thy

--- a/src/HOL/Relation.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Relation.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -420,7 +420,7 @@
 by blast
 
 lemma fst_eq_Domain: "fst ` R = Domain R"
-by (auto intro!:image_eqI)
+  by force
 
 lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
 by auto
@@ -471,7 +471,7 @@
 by blast
 
 lemma snd_eq_Range: "snd ` R = Range R"
-by (auto intro!:image_eqI)
+  by force
 
 
 subsection {* Field *}