src/Pure/Syntax/local_syntax.ML
changeset 62765 5b95a12b7b19
parent 62752 d09d71223e7a
child 80074 951c371c1cd9
--- 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