From 69bf0744a5ce3ba144f59564ebf74d7d2f56b748 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 15 Jun 2020 11:52:19 +0200
Subject: rename folders

---
 spartan/core/ml/types.ML | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 spartan/core/ml/types.ML

(limited to 'spartan/core/ml/types.ML')

diff --git a/spartan/core/ml/types.ML b/spartan/core/ml/types.ML
new file mode 100644
index 0000000..b0792fe
--- /dev/null
+++ b/spartan/core/ml/types.ML
@@ -0,0 +1,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
-- 
cgit v1.2.3