src/Pure/Syntax/mixfix.ML
changeset 62766 70b73465f636
parent 62761 5c672b22dcc2
child 62773 e6443edaebff
     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)];