# HG changeset patch
# User wenzelm
# Date 1413793190 -7200
# Node ID ca0b7d7cc9a37fa8ada937b18049f3e36389dce0
# Parent  7216a10d69ba807cfcb972cbf230b093072e581a
suppress special Poly/ML location inBasis (see $ML_SOURCES/mlsource/MLCompiler/STRUCT_VALS.ML);

diff -r 7216a10d69ba -r ca0b7d7cc9a3 src/Pure/ML/exn_properties_polyml.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 =