diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/Groups.thy	Mon Dec 09 12:22:23 2013 +0100
@@ -567,7 +567,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}
 *}