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