Lines Matching refs:trav
20 fun trav t =
25 (v, mk_comb(inst[alpha |-> type_of M] fun_tm,trav M),trav N)) M
26 else mk_plet (v, trav M, trav N)
30 mk_cond (J, trav M, trav N)
34 mk_pabs (trav M, trav N) end
37 trav tm
60 fun trav t =
64 mk_plet (v, mk_comb (inst [alpha |-> type_of M] fun_tm, trav M), trav N)
65 else mk_plet (v, trav M, trav N)
69 mk_cond (J, trav M, trav N)
73 mk_pabs (trav M, trav N) end
76 trav tm
81 fun trav t =
87 val (M',N') = (trav M, trav N)
95 else mk_plet (v, trav M, trav N)
99 mk_cond (J, trav M, trav N)
103 mk_pabs (trav M, trav N) end
106 trav tm