equal
deleted
inserted
replaced
142 then HOLogic.mk_list @{typ atom} [mk_atom t] |
142 then HOLogic.mk_list @{typ atom} [mk_atom t] |
143 else if is_atom_list ctxt ty |
143 else if is_atom_list ctxt ty |
144 then mk_atom_list t |
144 then mk_atom_list t |
145 else raise TERM ("listify", [t]) |
145 else raise TERM ("listify", [t]) |
146 end |
146 end |
147 |
|
148 (* coerces a list into a set *) |
|
149 fun to_set t = |
|
150 if fastype_of t = @{typ "atom list"} |
|
151 then @{term "set :: atom list => atom set"} $ t |
|
152 else t |
|
153 |
147 |
154 |
148 |
155 (** functions that construct the equations for fv and fv_bn **) |
149 (** functions that construct the equations for fv and fv_bn **) |
156 |
150 |
157 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = |
151 fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) = |