tuned messages -- position is usually missing here;

--- a/src/Pure/Isar/class.ML	Wed Mar 30 19:25:04 2016 +0200
+++ b/src/Pure/Isar/class.ML	Wed Mar 30 19:31:28 2016 +0200
@@ -617,9 +617,7 @@
   (case instantiation_param lthy b of
     SOME c =>
       if Mixfix.is_empty mx then lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
-      else
-        error ("Illegal mixfix syntax for overloaded constant " ^ quote c ^
-          Position.here (Mixfix.pos_of mx))
+      else error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
   | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
 
 fun pretty lthy =

--- a/src/Pure/Isar/overloading.ML	Wed Mar 30 19:25:04 2016 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Mar 30 19:31:28 2016 +0200
@@ -160,9 +160,7 @@
     SOME (c, (v, checked)) =>
       if Mixfix.is_empty mx then
         lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
-      else
-        error ("Illegal mixfix syntax for overloaded constant " ^ quote c ^
-          Position.here (Mixfix.pos_of mx))
+      else error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
   | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
 
 fun pretty lthy =

--- a/src/Pure/Syntax/local_syntax.ML	Wed Mar 30 19:25:04 2016 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Wed Mar 30 19:31:28 2016 +0200
@@ -83,8 +83,7 @@
       SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx)));
 
 fun prep_struct (Fixed, (c, _, Structure _)) = SOME c
-  | prep_struct (_, (c, _, mx as Structure _)) =
-      error ("Bad mixfix declaration for " ^ quote c ^ Position.here (Mixfix.pos_of mx))
+  | prep_struct (_, (c, _, Structure _)) = error ("Bad structure mixfix declaration for " ^ quote c)
   | prep_struct _ = NONE;
 
 in