--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Mon Dec 07 16:48:10 2015 +0000
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Mon Dec 07 20:19:59 2015 +0100
@@ -174,7 +174,7 @@
inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
eucl_le[where 'a='b] abs_prod_def abs_inner)
-text\<open>Instantiation for intervals on @{text ordered_euclidean_space}\<close>
+text\<open>Instantiation for intervals on \<open>ordered_euclidean_space\<close>\<close>
lemma
fixes a :: "'a::ordered_euclidean_space"