equal
deleted
inserted
replaced
619 |
619 |
620 fun alpha_ex_unroll (xlist, tm) = |
620 fun alpha_ex_unroll (xlist, tm) = |
621 let val (qvars,body) = S.strip_exists tm |
621 let val (qvars,body) = S.strip_exists tm |
622 val vlist = #2(S.strip_comb (S.rhs body)) |
622 val vlist = #2(S.strip_comb (S.rhs body)) |
623 val plist = ListPair.zip (vlist, xlist) |
623 val plist = ListPair.zip (vlist, xlist) |
624 val args = map (fn qv => valOf (gen_assoc (op aconv) (plist, qv))) qvars |
624 val args = map (the o AList.lookup (op aconv) plist) qvars |
625 handle Option => sys_error |
625 handle Option => sys_error |
626 "TFL fault [alpha_ex_unroll]: no correspondence" |
626 "TFL fault [alpha_ex_unroll]: no correspondence" |
627 fun build ex [] = [] |
627 fun build ex [] = [] |
628 | build (_$rex) (v::rst) = |
628 | build (_$rex) (v::rst) = |
629 let val ex1 = betapply(rex, v) |
629 let val ex1 = betapply(rex, v) |