diff -r d09d71223e7a -r 76b814ccce61 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Tue Mar 29 21:17:29 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Tue Mar 29 22:22:12 2016 +0200
@@ -7,7 +7,7 @@
 signature SYNTAX_EXT =
 sig
   val dddot_indexname: indexname
-  datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int
+  datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T
   val typ_to_nonterm: typ -> string
   datatype xsymb =
     Delim of string |
@@ -110,17 +110,15 @@
 
 (** datatype mfix **)
 
-(*Mfix (sy, ty, c, ps, p):
+(*Mfix (sy, ty, c, ps, p, pos):
     sy: rhs of production as symbolic text
     ty: type description of production
     c: head of parse tree
     ps: priorities of arguments in sy
-    p: priority of production*)
+    p: priority of production
+    pos: source position*)
 
-datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int;
-
-fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
-  cat_error msg ("in mixfix annotation " ^ quote (Symbol_Pos.content sy) ^ " for " ^ quote const);
+datatype mfix = Mfix of Symbol_Pos.T list * typ * string * int list * int * Position.T;
 
 
 (* typ_to_nonterm *)
@@ -189,13 +187,15 @@
 
 (* mfix_to_xprod *)
 
-fun mfix_to_xprod logical_types (mfix as Mfix (sy, typ, const, pris, pri)) =
+fun mfix_to_xprod logical_types (Mfix (sy, typ, const, pris, pri, pos)) =
   let
     val is_logtype = member (op =) logical_types;
 
+    fun err msg = error (msg ^ " in mixfix annotation" ^ Position.here pos);
+
     fun check_pri p =
       if p >= 0 andalso p <= 1000 then ()
-      else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
+      else err ("Precedence " ^ string_of_int p ^ " out of range");
 
     fun blocks_ok [] 0 = true
       | blocks_ok [] _ = false
@@ -206,21 +206,20 @@
 
     fun check_blocks syms =
       if blocks_ok syms 0 then ()
-      else err_in_mfix "Unbalanced block parentheses" mfix;
+      else err "Unbalanced block parentheses";
 
 
     val cons_fst = apfst o cons;
 
     fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
-      | add_args [] _ _ = err_in_mfix "Too many precedences" mfix
+      | add_args [] _ _ = err "Too many precedences"
       | add_args ((arg as Argument ("index", _)) :: syms) ty ps =
           cons_fst arg (add_args syms ty ps)
       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
           cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
           cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
-      | add_args (Argument _ :: _) _ _ =
-          err_in_mfix "More arguments than in corresponding type" mfix
+      | add_args (Argument _ :: _) _ _ = err "More arguments than in corresponding type"
       | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
 
     fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
@@ -231,7 +230,7 @@
       | logify_types a = a;
 
 
-    val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
+    val raw_symbs = read_mfix sy handle ERROR msg => err msg;
     val args = filter (fn Argument _ => true | _ => false) raw_symbs;
     val (const', typ', syntax_consts, parse_rules) =
       if not (exists is_index args) then (const, typ, NONE, NONE)
@@ -239,9 +238,9 @@
         let
           val indexed_const =
             if const <> "" then const ^ "_indexed"
-            else err_in_mfix "Missing constant name for indexed syntax" mfix;
+            else err "Missing constant name for indexed syntax";
           val rangeT = Term.range_type typ handle Match =>
-            err_in_mfix "Missing structure argument for indexed syntax" mfix;
+            err "Missing structure argument for indexed syntax";
 
           val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1));
           val (xs1, xs2) = chop (find_index is_index args) xs;
@@ -268,10 +267,10 @@
 
     val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
     val xprod' =
-      if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
+      if Lexicon.is_terminal lhs' then err ("Illegal lhs " ^ quote lhs')
       else if const <> "" then xprod
       else if length (filter is_argument symbs') <> 1 then
-        err_in_mfix "Copy production must have exactly one argument" mfix
+        err "Copy production must have exactly one argument"
       else if exists is_terminal symbs' then xprod
       else XProd (lhs', map rem_pri symbs', "", chain_pri);