equal
deleted
inserted
replaced
138 [(SOME bn, i)] => set (bn $ nth args i) |
138 [(SOME bn, i)] => set (bn $ nth args i) |
139 | _ => mk_union (map (fv_body thy dts args fv_frees false) (map snd binds)); |
139 | _ => mk_union (map (fv_body thy dts args fv_frees false) (map snd binds)); |
140 val non_rec_vars = |
140 val non_rec_vars = |
141 case binds of |
141 case binds of |
142 [(SOME bn, i)] => |
142 [(SOME bn, i)] => |
143 if i mem bodys |
143 if member (op =) bodys i |
144 then noatoms |
144 then noatoms |
145 else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i) |
145 else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i) |
146 | _ => noatoms |
146 | _ => noatoms |
147 in |
147 in |
148 mk_union [mk_diff fv_bodys bound_vars, non_rec_vars] |
148 mk_union [mk_diff fv_bodys bound_vars, non_rec_vars] |