# HG changeset patch
# User wenzelm
# Date 1331983579 -3600
# Node ID 15ce93dfe6da2cee59314ce90c180410b731e335
# Parent  8198cbff177191b1c0351b15291d15b4d92384a1
tuned message;

diff -r 8198cbff1771 -r 15ce93dfe6da src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sat Mar 17 12:21:15 2012 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Sat Mar 17 12:26:19 2012 +0100
@@ -178,7 +178,12 @@
       >> (fn ((ctxt, raw_c), Ts) =>
         let
           val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
-          val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
+          val consts = Proof_Context.consts_of ctxt;
+          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 "_")));
+          val const = Const (c, Consts.instance consts (c, Ts));
         in ML_Syntax.atomic (ML_Syntax.print_term const) end))));