src/HOLCF/Tools/Domain/domain_library.ML
 changeset 36692 54b64d4ad524 parent 35912 b0e300bd3a2c child 37145 01aa36932739
equal inserted replaced
`   226 fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);`
`   226 fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);`
`   227 `
`   227 `
`   228 fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) \$ Abs(a,T,body)) = `
`   228 fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) \$ Abs(a,T,body)) = `
`   229     (case cont_eta_contract body  of`
`   229     (case cont_eta_contract body  of`
`   230        body' as (Const("Cfun.Rep_CFun",Ta) \$ f \$ Bound 0) => `
`   230        body' as (Const("Cfun.Rep_CFun",Ta) \$ f \$ Bound 0) => `
`   231        if not (0 mem loose_bnos f) then incr_boundvars ~1 f `
`   231        if not (member (op =) (loose_bnos f) 0) then incr_boundvars ~1 f `
`   232        else   Const("Cfun.Abs_CFun",TT) \$ Abs(a,T,body')`
`   232        else   Const("Cfun.Abs_CFun",TT) \$ Abs(a,T,body')`
`   233      | body' => Const("Cfun.Abs_CFun",TT) \$ Abs(a,T,body'))`
`   233      | body' => Const("Cfun.Abs_CFun",TT) \$ Abs(a,T,body'))`
`   234   | cont_eta_contract(f\$t) = cont_eta_contract f \$ cont_eta_contract t`
`   234   | cont_eta_contract(f\$t) = cont_eta_contract f \$ cont_eta_contract t`
`   235   | cont_eta_contract t    = t;`
`   235   | cont_eta_contract t    = t;`
`   236 `
`   236 `