equal
deleted
inserted
replaced
65 |
65 |
66 fun map_consts f (Consts ({decls, constraints, rev_abbrevs, expand_abbrevs}, _)) = |
66 fun map_consts f (Consts ({decls, constraints, rev_abbrevs, expand_abbrevs}, _)) = |
67 make_consts (f (decls, constraints, rev_abbrevs, expand_abbrevs)); |
67 make_consts (f (decls, constraints, rev_abbrevs, expand_abbrevs)); |
68 |
68 |
69 fun abbrevs_of (Consts ({rev_abbrevs, ...}, _)) modes = |
69 fun abbrevs_of (Consts ({rev_abbrevs, ...}, _)) modes = |
70 List.concat (map (Symtab.lookup_list rev_abbrevs) modes); |
70 maps (Symtab.lookup_list rev_abbrevs) modes; |
71 |
71 |
72 |
72 |
73 (* dest consts *) |
73 (* dest consts *) |
74 |
74 |
75 fun dest_kind (LogicalConst _) = NONE |
75 fun dest_kind (LogicalConst _) = NONE |