1.1 --- a/src/Pure/ML/ml_antiquote.ML	Sat Mar 17 12:21:15 2012 +0100
     1.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sat Mar 17 12:26:19 2012 +0100
     1.3 @@ -178,7 +178,12 @@
     1.4        >> (fn ((ctxt, raw_c), Ts) =>
     1.5          let
     1.6            val Const (c, _) = Proof_Context.read_const_proper ctxt true raw_c;
     1.7 -          val const = Const (c, Consts.instance (Proof_Context.consts_of ctxt) (c, Ts));
     1.8 +          val consts = Proof_Context.consts_of ctxt;
     1.9 +          val n = length (Consts.typargs consts (c, Consts.type_scheme consts c));
    1.10 +          val _ = length Ts <> n andalso
    1.11 +            error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^
    1.12 +              quote c ^ enclose "(" ")" (commas (replicate n "_")));
    1.13 +          val const = Const (c, Consts.instance consts (c, Ts));
    1.14          in ML_Syntax.atomic (ML_Syntax.print_term const) end))));
    1.15  
    1.16