diff options
Diffstat (limited to 'spartan/core/ml/types.ML')
| -rw-r--r-- | spartan/core/ml/types.ML | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/spartan/core/ml/types.ML b/spartan/core/ml/types.ML deleted file mode 100644 index b0792fe..0000000 --- a/spartan/core/ml/types.ML +++ /dev/null @@ -1,18 +0,0 @@ -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 |