src/HOL/Rings.thy

--- a/src/HOL/Rings.thy	Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Rings.thy	Mon Dec 09 12:22:23 2013 +0100
@@ -449,7 +449,7 @@
   \end{itemize}
   Most of the used notions can also be looked up in 
   \begin{itemize}
-  \item \url{http://www.mathworld.com} by Eric Weisstein et. al.
+  \item @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
   \item \emph{Algebra I} by van der Waerden, Springer.
   \end{itemize}
 *}