equal
deleted
inserted
replaced
97 fun mk_atom_fset t = |
97 fun mk_atom_fset t = |
98 let |
98 let |
99 val ty = fastype_of t; |
99 val ty = fastype_of t; |
100 val atom_ty = dest_fsetT ty --> @{typ "atom"}; |
100 val atom_ty = dest_fsetT ty --> @{typ "atom"}; |
101 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
101 val fmap_ty = atom_ty --> ty --> @{typ "atom fset"}; |
102 val fset_to_set = @{term "fset_to_set :: atom fset => atom set"} |
102 val fset = @{term "fset :: atom fset => atom set"} |
103 in |
103 in |
104 fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
104 fset $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t) |
105 end |
105 end |
106 |
106 |
107 fun mk_atom_list t = |
107 fun mk_atom_list t = |
108 let |
108 let |
109 val ty = fastype_of t; |
109 val ty = fastype_of t; |