# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1307362264 -3600
# Node ID 77e1d9f2925e022e54da50a5ca33adec871d11e0
# Parent  4bd584ff4fab57d34df7acf5224c438b6ec4f148
slightly stronger property in fundef_ex_prop

diff -r 4bd584ff4fab -r 77e1d9f2925e Nominal/Nominal2_Base.thy
--- 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)