# HG changeset patch
# User wenzelm
# Date 1632858098 -7200
# Node ID 6cefe97cb3abea251461aefa2e2c4ba1ca5aeab2
# Parent  1cc6309401478495412fdd1c2b2ae1b2a5b9f4ba
clarified message;

diff -r 1cc630940147 -r 6cefe97cb3ab src/Pure/ML/ml_antiquotations1.ML
--- a/src/Pure/ML/ml_antiquotations1.ML	Tue Sep 28 17:12:53 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations1.ML	Tue Sep 28 21:41:38 2021 +0200
@@ -328,7 +328,7 @@
           length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)");
         val _ =
           length term_args > m andalso Term.is_Type (Term.body_type T) andalso
-            err (" cannot have more than " ^ string_of_int m ^ " type argument(s)");
+            err (" cannot have more than " ^ string_of_int m ^ " argument(s)");
 
         val (decls1, ctxt1) = ml_args ctxt type_args;
         val (decls2, ctxt2) = ml_args ctxt1 term_args;