# HG changeset patch
# User haftmann
# Date 1236237790 -3600
# Node ID 9c4f4ac0d03856420c7b46afd6db466abd43e6a2
# Parent  5ffa9d4dbea75931aa58e03e7d746d8fc47af2b9
tuned

diff -r 5ffa9d4dbea7 -r 9c4f4ac0d038 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Thu Mar 05 08:23:09 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Thu Mar 05 08:23:10 2009 +0100
@@ -4396,7 +4396,7 @@
   assumes iB: "independent (B:: (real ^'n) set)"
   shows "\<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x)"
 proof-
-  from maximal_independent_subset_extend[of B "UNIV"] iB
+  from maximal_independent_subset_extend[of B UNIV] iB
   obtain C where C: "B \<subseteq> C" "independent C" "\<And>x. x \<in> span C" by auto
   
   from C(2) independent_bound[of C] linear_independent_extend_lemma[of C f]