diff -r c1b88e647e2f -r d97e13e5ea5b src/Pure/ML/exn_properties.ML
--- a/src/Pure/ML/exn_properties.ML	Mon Feb 29 15:23:13 2016 +0100
+++ b/src/Pure/ML/exn_properties.ML	Mon Feb 29 15:39:17 2016 +0100
@@ -21,7 +21,7 @@
     [] => []
   | [XML.Text file] =>
       if file = "Standard Basis" then []
-      else [(Markup.fileN, ml_standard_path file)]
+      else [(Markup.fileN, ML_System.standard_path file)]
   | body => XML.Decode.properties body);
 
 fun position_of loc =