avoid duplicate reports;
authorwenzelm
Wed Mar 30 20:35:35 2016 +0200 (2016-03-30)
changeset 6276670b73465f636
parent 62765 5b95a12b7b19
child 62767 d6b0d35b3aed
avoid duplicate reports;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 19:31:28 2016 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 20:35:35 2016 +0200
     1.3 @@ -164,8 +164,8 @@
     1.4    let
     1.5      fun mk_infix sy ty c p1 p2 p3 range =
     1.6        [Syntax_Ext.Mfix
     1.7 -        (Symbol_Pos.explode0 "op " @ Input.source_explode sy,
     1.8 -          ty, c, [], 1000, Position.set_range range),
     1.9 +        (Symbol_Pos.explode0 "op " @ Input.source_explode (Input.reset_pos sy),
    1.10 +          ty, c, [], 1000, Position.none),
    1.11         Syntax_Ext.Mfix
    1.12          (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
    1.13            ty, c, [p1, p2], p3, Position.set_range range)];