# HG changeset patch
# User wenzelm
# Date 1482489401 -3600
# Node ID 84aea854dc3cf8f5c15272f97a9d462098fad664
# Parent  ef85bb6491b30cd75758b7d092882235c28bdb86
suppress dummy id;

diff -r ef85bb6491b3 -r 84aea854dc3c src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Fri Dec 23 11:21:38 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Fri Dec 23 11:36:41 2016 +0100
@@ -86,7 +86,7 @@
       let
         val pos = Exn_Properties.position_of_polyml_location loc;
       in
-        is_reported pos ?
+        (is_reported pos andalso id <> 0) ?
           let
             fun markup () =
               (Markup.entityN, [(if def then Markup.defN else Markup.refN, Value.print_int id)]);