File ‹UD_Consts.ML›
signature UD_CONSTS =
sig
structure ConstsData : THEORY_DATA
val const_of_key : theory -> Symtab.key -> term option
val update_const : Symtab.key -> term -> theory -> theory
val remove_const : Symtab.key -> theory -> theory
val get_keys : theory -> Symtab.key list
end;
structure UD_Consts : UD_CONSTS =
struct
structure ConstsData = Theory_Data
(
type T = term Symtab.table
val empty = Symtab.empty
val merge = Symtab.merge (K true)
)
val const_of_key = Symtab.lookup o ConstsData.get
fun update_const k v = ConstsData.map (Symtab.update (k, v))
fun remove_const k = ConstsData.map (Symtab.delete k)
val get_keys = Symtab.keys o ConstsData.get
end;