Lemma "fundef_default_value" uses predicate instead of set.

--- a/src/HOL/FunDef.thy	Fri Nov 24 13:43:44 2006 +0100
+++ b/src/HOL/FunDef.thy	Fri Nov 24 13:44:51 2006 +0100
@@ -149,14 +149,15 @@
 
 lemma fundef_default_value:
 assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (\<lambda>y. G x y))"
-assumes graph: "\<And>x y. G x y \<Longrightarrow> x \<in> D"
-assumes "x \<notin> D"
+assumes graph: "\<And>x y. G x y \<Longrightarrow> D x"
+assumes "\<not> D x"
 shows "f x = d x"
 proof -
   have "\<not>(\<exists>y. G x y)"
   proof
-    assume "(\<exists>y. G x y)"
-    with graph and `x\<notin>D` show False by blast
+    assume "\<exists>y. G x y"
+    hence "D x" using graph ..
+    with `\<not> D x` show False ..
   qed
   hence "\<not>(\<exists>!y. G x y)" by blast