tuned;

--- a/src/Pure/Isar/parse.ML	Wed Mar 30 14:52:23 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Wed Mar 30 14:59:12 2016 +0200
@@ -320,29 +320,29 @@
 val mfix =
   input string --
     !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] -- Scan.optional nat 1000)
-  >> (fn (sy, (ps, p)) => Mixfix (sy, ps, p, Position.no_range));
+  >> (fn (sy, (ps, p)) => fn range => Mixfix (sy, ps, p, range));
 
 val infx =
-  $$$ "infix" |-- !!! (input string -- nat >> (fn (sy, p) => Infix (sy, p, Position.no_range)));
+  $$$ "infix" |-- !!! (input string -- nat >> (fn (sy, p) => fn range => Infix (sy, p, range)));
 
 val infxl =
-  $$$ "infixl" |-- !!! (input string -- nat >> (fn (sy, p) => Infixl (sy, p, Position.no_range)));
+  $$$ "infixl" |-- !!! (input string -- nat >> (fn (sy, p) => fn range => Infixl (sy, p, range)));
 
 val infxr =
-  $$$ "infixr" |-- !!! (input string -- nat >> (fn (sy, p) => Infixr (sy, p, Position.no_range)));
+  $$$ "infixr" |-- !!! (input string -- nat >> (fn (sy, p) => fn range => Infixr (sy, p, range)));
 
-val strcture = $$$ "structure" >> K (Structure Position.no_range);
+val strcture = $$$ "structure" >> K Structure;
 
 val binder =
   $$$ "binder" |--
     !!! (input string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
-  >> (fn (sy, (p, q)) => Binder (sy, p, q, Position.no_range));
+  >> (fn (sy, (p, q)) => fn range => Binder (sy, p, q, range));
 
 val mixfix_body = mfix || strcture || binder || infxl || infxr || infx;
 
 fun annotation guard body =
   Scan.trace ($$$ "(" |-- guard (body --| $$$ ")"))
-    >> (fn (mx, toks) => Mixfix.set_range (Token.range_of toks) mx);
+    >> (fn (mx, toks) => mx (Token.range_of toks));
 
 fun opt_annotation guard body = Scan.optional (annotation guard body) NoSyn;
 

--- a/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:52:23 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Mar 30 14:59:12 2016 +0200
@@ -22,7 +22,6 @@
   include BASIC_MIXFIX
   val is_empty: mixfix -> bool
   val equal: mixfix * mixfix -> bool
-  val set_range: Position.range -> mixfix -> mixfix
   val range_of: mixfix -> Position.range
   val pos_of: mixfix -> Position.T
   val reset_pos: mixfix -> mixfix
@@ -65,17 +64,6 @@
   | equal (Structure _, Structure _) = true
   | equal _ = false;
 
-fun set_range range mx =
-  (case mx of
-    NoSyn => NoSyn
-  | Mixfix (sy, ps, p, _) => Mixfix (sy, ps, p, range)
-  | Delimfix (sy, _) => Delimfix (sy, range)
-  | Infix (sy, p, _) => Infix (sy, p, range)
-  | Infixl (sy, p, _) => Infixl (sy, p, range)
-  | Infixr (sy, p, _) => Infixr (sy, p, range)
-  | Binder (sy, p, q, _) => Binder (sy, p, q, range)
-  | Structure _ => Structure range);
-
 fun range_of NoSyn = Position.no_range
   | range_of (Mixfix (_, _, _, range)) = range
   | range_of (Delimfix (_, range)) = range