# HG changeset patch
# User wenzelm
# Date 1474204790 -7200
# Node ID e4fdf95803726c0e34a47fdfe542c65aee6d6859
# Parent  cc15bd7c5396b31b170a9e670f37e183a0ad5a0e
tuned;

diff -r cc15bd7c5396 -r e4fdf9580372 src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Sun Sep 18 15:16:42 2016 +0200
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Sun Sep 18 15:19:50 2016 +0200
@@ -479,7 +479,7 @@
   interpret vectorspace E by fact
   interpret subspace H E by fact
   from x y x' have "x \<in> H + lin x'" by auto
-  have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
+  have "\<exists>!(y, a). x = y + a \<cdot> x' \<and> y \<in> H" (is "\<exists>!p. ?P p")
   proof (rule ex_ex1I)
     from x y show "\<exists>p. ?P p" by blast
     fix p q assume p: "?P p" and q: "?P q"