equal
deleted
inserted
replaced
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' = |