src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy

--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Sun Dec 14 18:45:51 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Dec 15 18:12:52 2008 +0100
@@ -405,10 +405,10 @@
     and "linearform H h"
   shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
 proof
-  interpret subspace [H E] by fact
-  interpret vectorspace [E] by fact
-  interpret seminorm [E p] by fact
-  interpret linearform [H h] by fact
+  interpret subspace H E by fact
+  interpret vectorspace E by fact
+  interpret seminorm E p by fact
+  interpret linearform H h by fact
   have H: "vectorspace H" using `vectorspace E` ..
   {
     assume l: ?L