equal
deleted
inserted
replaced
62 val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; |
62 val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"}; |
63 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
63 val img_ty = atom_ty --> ty --> @{typ "atom set"}; |
64 in |
64 in |
65 Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t |
65 Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t |
66 end |
66 end |
|
67 |
|
68 |
|
69 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
|
70 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
67 |
71 |
68 fun mk_atom_fset t = |
72 fun mk_atom_fset t = |
69 let |
73 let |
70 val ty = fastype_of t; |
74 val ty = fastype_of t; |
71 val atom_ty = dest_fsetT ty --> @{typ "atom"}; |
75 val atom_ty = dest_fsetT ty --> @{typ "atom"}; |