suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);
--- a/src/Pure/ML/exn_properties_polyml.ML Mon Oct 20 07:45:58 2014 +0200
+++ b/src/Pure/ML/exn_properties_polyml.ML Mon Oct 20 10:19:50 2014 +0200
@@ -19,7 +19,9 @@
fun props_of (loc: PolyML.location) =
(case YXML.parse_body (#file loc) of
[] => []
- | [XML.Text file] => [(Markup.fileN, file)]
+ | [XML.Text file] =>
+ if file = "Standard Basis" then []
+ else [(Markup.fileN, file)]
| body => XML.Decode.properties body);
fun position_of loc =