# HG changeset patch
# User wenzelm
# Date 1459362935 -7200
# Node ID 70b73465f636230d0321f1ead4673fb1aec9308b
# Parent  5b95a12b7b19d0da6da16173b9e000230f2de20d
avoid duplicate reports;

diff -r 5b95a12b7b19 -r 70b73465f636 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 19:31:28 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 20:35:35 2016 +0200
@@ -164,8 +164,8 @@
   let
     fun mk_infix sy ty c p1 p2 p3 range =
       [Syntax_Ext.Mfix
-        (Symbol_Pos.explode0 "op " @ Input.source_explode sy,
-          ty, c, [], 1000, Position.set_range range),
+        (Symbol_Pos.explode0 "op " @ Input.source_explode (Input.reset_pos sy),
+          ty, c, [], 1000, Position.none),
        Syntax_Ext.Mfix
         (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)",
           ty, c, [p1, p2], p3, Position.set_range range)];