diff -r 1f4d6870b7b2 -r f0ee92285221 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Sun Sep 29 12:44:40 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Sun Sep 29 12:49:47 2013 +0200
@@ -2086,7 +2086,7 @@
 text {*
   %FIXME
 
-  See also @{"file" "~~/src/Pure/Concurrent/lazy.ML"}.
+  See also @{file "~~/src/Pure/Concurrent/lazy.ML"}.
 *}
 
 
@@ -2095,7 +2095,7 @@
 text {*
   %FIXME
 
-  See also @{"file" "~~/src/Pure/Concurrent/future.ML"}.
+  See also @{file "~~/src/Pure/Concurrent/future.ML"}.
 *}