equal
deleted
inserted
replaced
510 fun alpha_ex_unroll (xlist, tm) = |
510 fun alpha_ex_unroll (xlist, tm) = |
511 let val (qvars,body) = S.strip_exists tm |
511 let val (qvars,body) = S.strip_exists tm |
512 val vlist = #2(S.strip_comb (S.rhs body)) |
512 val vlist = #2(S.strip_comb (S.rhs body)) |
513 val plist = ListPair.zip (vlist, xlist) |
513 val plist = ListPair.zip (vlist, xlist) |
514 val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars |
514 val args = map (fn qv => the (gen_assoc (op aconv) (plist, qv))) qvars |
515 handle OPTION _ => error |
515 handle OPTION => error |
516 "TFL fault [alpha_ex_unroll]: no correspondence" |
516 "TFL fault [alpha_ex_unroll]: no correspondence" |
517 fun build ex [] = [] |
517 fun build ex [] = [] |
518 | build (_$rex) (v::rst) = |
518 | build (_$rex) (v::rst) = |
519 let val ex1 = betapply(rex, v) |
519 let val ex1 = betapply(rex, v) |
520 in ex1 :: build ex1 rst |
520 in ex1 :: build ex1 rst |