equal
deleted
inserted
replaced
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 fun bound_var (SOME bn, i) = set (bn $ nth args i) |
136 fun bound_var (SOME bn, i) = set (bn $ nth args i) |
137 | bound_var (NONE, i) = fv_body thy dts args fv_frees false i |
137 | bound_var (NONE, i) = fv_body thy dts args fv_frees false i |
138 val bound_vars = mk_union (map bound_var binds); |
138 val bound_vars = mk_union (map bound_var binds); |
139 val non_rec_vars = |
139 fun non_rec_var (SOME bn, i) = |
140 case binds of |
140 if member (op =) bodys i |
141 [(SOME bn, i)] => |
141 then noatoms |
142 if member (op =) bodys i |
142 else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i) |
143 then noatoms |
143 | non_rec_var (NONE, _) = noatoms |
144 else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i) |
144 in |
145 | _ => noatoms |
145 mk_union ((mk_diff fv_bodys bound_vars) :: (map non_rec_var binds)) |
146 in |
|
147 mk_union [mk_diff fv_bodys bound_vars, non_rec_vars] |
|
148 end |
146 end |
149 *} |
147 *} |
150 |
148 |
151 ML {* |
149 ML {* |
152 fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm = |
150 fun fv_bn_bm thy dts args fv_frees bn_fvbn args_in_bn bm = |