equal
deleted
inserted
replaced
131 |
131 |
132 ML {* |
132 ML {* |
133 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = |
133 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys = |
134 let |
134 let |
135 val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys) |
135 val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys) |
136 val bound_vars = |
136 fun bound_var (SOME bn, i) = set (bn $ nth args i) |
137 case binds of |
137 | bound_var (NONE, i) = fv_body thy dts args fv_frees false i |
138 [(SOME bn, i)] => set (bn $ nth args i) |
138 val bound_vars = mk_union (map bound_var binds); |
139 | _ => mk_union (map (fv_body thy dts args fv_frees false) (map snd binds)); |
|
140 val non_rec_vars = |
139 val non_rec_vars = |
141 case binds of |
140 case binds of |
142 [(SOME bn, i)] => |
141 [(SOME bn, i)] => |
143 if member (op =) bodys i |
142 if member (op =) bodys i |
144 then noatoms |
143 then noatoms |