equal
deleted
inserted
replaced
168 fun qconsts_update_gen id qcinfo = Context.mapping (qconsts_update_thy id qcinfo) I |
168 fun qconsts_update_gen id qcinfo = Context.mapping (qconsts_update_thy id qcinfo) I |
169 |
169 |
170 fun qconsts_dest thy = |
170 fun qconsts_dest thy = |
171 map snd (Symtab.dest (QConstsData.get thy)) |
171 map snd (Symtab.dest (QConstsData.get thy)) |
172 |
172 |
|
173 (* FIXME / TODO : better implementation of the lookup datastructure *) |
|
174 (* for example symtabs to alist; or tables with string type key *) |
173 fun qconsts_lookup thy t = |
175 fun qconsts_lookup thy t = |
174 let |
176 let |
175 val smt = Symtab.dest (QConstsData.get thy); |
177 val smt = Symtab.dest (QConstsData.get thy); |
176 val (name, qty) = dest_Const t |
178 val (name, qty) = dest_Const t |
177 fun matches (_, x) = |
179 fun matches (_, x) = |