changeset 62468 | d97e13e5ea5b |
parent 62387 | ad3eb2889f9a |
child 62516 | 5732f1c31566 |
--- 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 =