--- 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