author | wenzelm |
Tue, 08 Sep 2015 21:49:21 +0200 | |
changeset 61138 | dcbec1b22b07 |
parent 61137 | 4010e1559a24 |
child 61139 | f9fd43d8981d |
--- 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 =