diff -r 82356c9e218a -r 068a01b4bc56 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat Apr 24 11:11:09 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat Apr 24 13:31:52 2010 -0700
@@ -114,7 +114,7 @@
   instance by (intro_classes)
 end
 
-text{* The ordering on real^1 is linear. *}
+text{* The ordering on @{typ "real^1"} is linear. *}
 
 class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
 begin