--- a/Nominal/Nominal2_Base.thy	Sun Jun 05 21:14:23 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Mon Jun 06 13:11:04 2011 +0100
@@ -1742,9 +1742,9 @@
 lemma fundef_ex1_prop:
   fixes x::"'a::pt"
   assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
-  assumes P_all: "\<And>y. G x y \<Longrightarrow> P y"
+  assumes P_all: "\<And>x y. G x y \<Longrightarrow> P x y"
   assumes ex1: "\<exists>!y. G x y"
-  shows "P (f x)"
+  shows "P x (f x)"
   unfolding f_def
   using ex1
   apply(erule_tac ex1E)