diff -r c33faa289520 -r 3a0a65ca2261 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Aug 31 20:34:44 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Mon Aug 31 20:34:48 2009 +0200
@@ -630,9 +630,6 @@
 apply blast
 done
 
-lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
-  by (auto simp:inv_image_def)
-
 text {* Measure Datatypes into @{typ nat} *}
 
 definition measure :: "('a => nat) => ('a * 'a)set"