# HG changeset patch
# User wenzelm
# Date 1395508328 -3600
# Node ID 73e2e1912571c3ea269c61210c97b470833d0b4c
# Parent  2c9f841f36b8926885001da21a29b16ee9ad0be0
tuned message;

diff -r 2c9f841f36b8 -r 73e2e1912571 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sat Mar 22 16:50:52 2014 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Sat Mar 22 18:12:08 2014 +0100
@@ -121,9 +121,9 @@
       else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
 
   ML_Antiquotation.inline @{binding const}
-    (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional
+    (Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) -- Scan.optional
         (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) []
-      >> (fn ((ctxt, raw_c), Ts) =>
+      >> (fn ((ctxt, (raw_c, pos)), Ts) =>
         let
           val Const (c, _) =
             Proof_Context.read_const {proper = true, strict = true} ctxt raw_c;
@@ -131,7 +131,7 @@
           val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
           val _ = length Ts <> n andalso
             error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
-              quote c ^ enclose "(" ")" (commas (replicate n "_")));
+              quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos);
           val const = Const (c, Consts.instance consts (c, Ts));
         in ML_Syntax.atomic (ML_Syntax.print_term const) end)));