blob: b0792feb1f7c8045b6a9b627ae1d0ea6e4aabd64 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
structure Types
= struct
structure Data = Generic_Data (
type T = thm Item_Net.T
val empty = Item_Net.init Thm.eq_thm
(single o Lib.term_of_typing o Thm.prop_of)
val extend = I
val merge = Item_Net.merge
)
fun put_type typing = Context.proof_map (Data.map (Item_Net.update typing))
fun put_types typings = foldr1 (op o) (map put_type typings)
fun get_types ctxt tm = Item_Net.retrieve (Data.get (Context.Proof ctxt)) tm
end
|
