--- a/src/HOL/Hahn_Banach/Function_Order.thy Tue Oct 21 10:58:19 2014 +0200
+++ b/src/HOL/Hahn_Banach/Function_Order.thy Tue Oct 21 11:13:16 2014 +0200
@@ -102,7 +102,7 @@
definition
norm_pres_extensions ::
- "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
+ "'a::{plus,minus,uminus,zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
\<Rightarrow> 'a graph set"
where
"norm_pres_extensions E p F f