--- a/src/Pure/ML/ml_compiler_polyml.ML Tue Nov 11 21:14:19 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML Wed Nov 12 10:30:59 2014 +0100
@@ -32,10 +32,12 @@
end;
fun reported_entity kind loc decl =
- let val pos = Exn_Properties.position_of loc in
- is_reported pos ?
+ let
+ val pos = Exn_Properties.position_of loc;
+ val def_pos = Exn_Properties.position_of decl;
+ in
+ (is_reported pos andalso pos <> def_pos) ?
let
- val def_pos = Exn_Properties.position_of decl;
fun markup () =
(Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
in cons (pos, markup, fn () => "") end