src/HOLCF/Tools/Domain/domain_library.ML
changeset 36692 54b64d4ad524
parent 35912 b0e300bd3a2c
child 37145 01aa36932739
equal deleted inserted replaced
36674:d95f39448121 36692:54b64d4ad524
   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