1 files changed, 3 insertions, 60 deletions
diff --git a/spartan/core/types.ML b/spartan/core/types.ML
index a521f7c..70e5057 100644
--- a/spartan/core/types.ML
+++ b/spartan/core/types.ML
@@ -1,23 +1,11 @@
-(*  Title:      typechecking.ML
+(*  Title:      types.ML
     Author:     Joshua Chen
 
-Type information and type-checking infrastructure.
+Type-checking infrastructure.
 *)
 
 structure Types: sig
 
-val Known: Proof.context -> thm Item_Net.T
-val known: Proof.context -> thm list
-val known_of: Proof.context -> term -> thm list
-val register_known: thm -> Context.generic -> Context.generic
-val register_knowns: thm list -> Context.generic -> Context.generic
-
-val Cond: Proof.context -> thm Item_Net.T
-val cond: Proof.context -> thm list
-val cond_of: Proof.context -> term -> thm list
-val register_cond: thm -> Context.generic -> Context.generic
-val register_conds: thm list -> Context.generic -> Context.generic
-
 val debug_typechk: bool Config.T
 
 val known_ctac: thm list -> int -> context_tactic
@@ -25,52 +13,7 @@ val check_infer: thm list -> int -> context_tactic
 
 end = struct
 
-
-(** Context data **)
-
-(* Known types *)
-
-structure Known = 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
-)
-
-val Known = Known.get o Context.Proof
-val known = Item_Net.content o Known
-fun known_of ctxt tm = Item_Net.retrieve (Known ctxt) tm
-
-fun register_known typing =
-  if Lib.is_typing (Thm.prop_of typing) then Known.map (Item_Net.update typing)
-  else error "Not a type judgment"
-
-fun register_knowns typings = foldr1 (op o) (map register_known typings)
-
-(* Conditional type rules *)
-
-(*Two important cases: 1. general type inference rules and 2. type family
-  judgments*)
-
-structure Cond = Generic_Data (
-  type T = thm Item_Net.T
-  val empty = Item_Net.init Thm.eq_thm
-    (single o Lib.term_of_typing o Thm.concl_of)
-  val extend = I
-  val merge = Item_Net.merge
-)
-
-val Cond = Cond.get o Context.Proof
-val cond = Item_Net.content o Cond
-fun cond_of ctxt tm = Item_Net.retrieve (Cond ctxt) tm
-
-fun register_cond rule =
-  if Lib.is_typing (Thm.concl_of rule) then Cond.map (Item_Net.update rule)
-  else error "Not a conditional type judgment"
-
-fun register_conds rules = foldr1 (op o) (map register_cond rules)
-
+open Context_Facts
 
 (** [type] attribute **)