equal
deleted
inserted
replaced
16 |
16 |
17 (* table of specialisations *) |
17 (* table of specialisations *) |
18 structure Specialisations = Theory_Data |
18 structure Specialisations = Theory_Data |
19 ( |
19 ( |
20 type T = (term * term) Item_Net.T; |
20 type T = (term * term) Item_Net.T; |
21 val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool) |
21 val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); |
22 (single o fst); |
|
23 val extend = I; |
22 val extend = I; |
24 val merge = Item_Net.merge; |
23 val merge = Item_Net.merge; |
25 ) |
24 ) |
26 |
25 |
27 fun specialisation_of thy atom = |
26 fun specialisation_of thy atom = |