1.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Sun Dec 14 18:45:51 2008 +0100
     1.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Dec 15 18:12:52 2008 +0100
     1.3 @@ -405,10 +405,10 @@
     1.4      and "linearform H h"
     1.5    shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
     1.6  proof
     1.7 -  interpret subspace [H E] by fact
     1.8 -  interpret vectorspace [E] by fact
     1.9 -  interpret seminorm [E p] by fact
    1.10 -  interpret linearform [H h] by fact
    1.11 +  interpret subspace H E by fact
    1.12 +  interpret vectorspace E by fact
    1.13 +  interpret seminorm E p by fact
    1.14 +  interpret linearform H h by fact
    1.15    have H: "vectorspace H" using `vectorspace E` ..
    1.16    {
    1.17      assume l: ?L