equal
deleted
inserted
replaced
11 | BRes of ((term option * int) list) * (int list) |
11 | BRes of ((term option * int) list) * (int list) |
12 *} |
12 *} |
13 |
13 |
14 ML {* |
14 ML {* |
15 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
15 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *); |
16 (* TODO: It is the same as one in 'nominal_atoms' *) |
16 |
17 fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom}); |
17 fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom x]; |
18 fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]; |
|
19 val noatoms = @{term "{} :: atom set"}; |
18 val noatoms = @{term "{} :: atom set"}; |
20 fun mk_union sets = |
19 fun mk_union sets = |
21 fold (fn a => fn b => |
20 fold (fn a => fn b => |
22 if a = noatoms then b else |
21 if a = noatoms then b else |
23 if b = noatoms then a else |
22 if b = noatoms then a else |