src/Pure/ML/ml_antiquotations1.ML
changeset 74377 6cefe97cb3ab
parent 74374 e585e5a906ba
child 74378 bb25ea271b15
equal deleted inserted replaced
74376:1cc630940147 74377:6cefe97cb3ab
   326             Position.here (Input.pos_of s));
   326             Position.here (Input.pos_of s));
   327         val _ =
   327         val _ =
   328           length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)");
   328           length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)");
   329         val _ =
   329         val _ =
   330           length term_args > m andalso Term.is_Type (Term.body_type T) andalso
   330           length term_args > m andalso Term.is_Type (Term.body_type T) andalso
   331             err (" cannot have more than " ^ string_of_int m ^ " type argument(s)");
   331             err (" cannot have more than " ^ string_of_int m ^ " argument(s)");
   332 
   332 
   333         val (decls1, ctxt1) = ml_args ctxt type_args;
   333         val (decls1, ctxt1) = ml_args ctxt type_args;
   334         val (decls2, ctxt2) = ml_args ctxt1 term_args;
   334         val (decls2, ctxt2) = ml_args ctxt1 term_args;
   335         val (decls3, ctxt3) = ml_args ctxt2 fn_body;
   335         val (decls3, ctxt3) = ml_args ctxt2 fn_body;
   336         fun decl' ctxt' =
   336         fun decl' ctxt' =