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 =