suppress dummy id;
authorwenzelm
Fri, 23 Dec 2016 11:36:41 +0100 (2016-12-23)
changeset 64661 84aea854dc3c
parent 64660 ef85bb6491b3
child 64662 5a2c15faf89c
suppress dummy id;
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)]);