TFL/tfl.sml
changeset 4149 a6ccec4fd0c3
parent 4062 fa2eb95b1b2d
child 4221 ed0f67fb458b
equal deleted inserted replaced
4148:e0e5a2820ac1 4149:a6ccec4fd0c3
   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