src/Pure/ML/exn_properties_polyml.ML

--- a/src/Pure/ML/exn_properties_polyml.ML	Tue Sep 08 21:10:23 2015 +0200
+++ b/src/Pure/ML/exn_properties_polyml.ML	Tue Sep 08 21:49:21 2015 +0200
@@ -21,7 +21,7 @@
     [] => []
   | [XML.Text file] =>
       if file = "Standard Basis" then []
-      else [(Markup.fileN, file)]
+      else [(Markup.fileN, ml_standard_path file)]
   | body => XML.Decode.properties body);
 
 fun position_of loc =