equal
deleted
inserted
replaced
129 fun mk_atom_fset_ty ty t = |
129 fun mk_atom_fset_ty ty t = |
130 let |
130 let |
131 val atom_ty = dest_fsetT ty |
131 val atom_ty = dest_fsetT ty |
132 val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; |
132 val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"}; |
133 in |
133 in |
134 Const (@{const_name map_fset}, fmap_ty) $ atom_const atom_ty $ t |
134 Const (@{const_name fimage}, fmap_ty) $ atom_const atom_ty $ t |
135 end |
135 end |
136 |
136 |
137 fun mk_atom_list_ty ty t = |
137 fun mk_atom_list_ty ty t = |
138 let |
138 let |
139 val atom_ty = dest_listT ty |
139 val atom_ty = dest_listT ty |