Lines Matching refs:args
426 let val (f,args) = strip_comb term
428 foldl (fn (a,b) => beta_conv (mk_comb(b,a))) f args
1488 val (type_subst,args) =
1490 let val args = with_exn (snd o strip_comb o rator) func exn1
1493 (res_t |-> list_mk_fun(map type_of args,type_of func),args)
1502 args thm_clauses handle e => wrap "" e;
1506 let val args = snd (strip_comb (lhs (concl tc)))
1508 (repeat rator func |-> list_mk_abs(tl args,(mk_abs(hd args,lhs (concl tc))))) end)