diff -r 3daeba5130f0 -r 499f92dc6e45 src/HOL/ex/Sudoku.thy
--- a/src/HOL/ex/Sudoku.thy	Mon Dec 09 12:16:52 2013 +0100
+++ b/src/HOL/ex/Sudoku.thy	Mon Dec 09 12:22:23 2013 +0100
@@ -137,7 +137,7 @@
 
 text {*
   Some "exceptionally difficult" Sudokus, taken from
-  \url{http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903}
+  @{url "http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903"}
   (accessed December 2, 2008).
 *}