Lines Matching refs:f2
13 fun mk_seq(f1,f2) =
15 val (d2,r2) = dom_rng (type_of f2)
17 list_mk_comb(inst[alpha|->d1,beta|->r1,gamma |-> r2]seq_tm,[f1,f2])
21 fun mk_par(f1,f2) =
23 val (d2,r2) = dom_rng (type_of f2)
25 list_mk_comb(inst[alpha|->d1,beta|->r1,gamma |-> r2]par_tm,[f1,f2])
29 fun mk_ite(f1,f2,f3) =
31 val (_,r2) = dom_rng (type_of f2)
33 list_mk_comb(inst[alpha|->d1,beta|->r2]ite_tm,[f1,f2,f3])
37 fun mk_rec(f1,f2,f3) =
39 val (_,r2) = dom_rng (type_of f2)
41 list_mk_comb(inst[alpha|->d1,beta|->r2]rec_tm,[f1,f2,f3])