From d172f9d35a9a1680ec15e4c61e5becbbc92d2ce7 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 14 Aug 2020 11:21:59 +0200
Subject: reorganize

---
 spartan/core/tactics.ML | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'spartan/core/tactics.ML')

diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML
index 0c46ef0..923a3a7 100644
--- a/spartan/core/tactics.ML
+++ b/spartan/core/tactics.ML
@@ -111,7 +111,7 @@ fun elim_ctac tms =
     [] => CONTEXT_TACTIC' (fn ctxt => eresolve_tac ctxt (map #1 (Elim.rules ctxt)))
   | major :: _ => CONTEXT_SUBGOAL (fn (goal, _) => fn cst as (ctxt, st) =>
       let
-        val facts = map Thm.prop_of (Types.known ctxt)
+        val facts = map Thm.prop_of (Context_Facts.known ctxt)
         val prems = Logic.strip_assums_hyp goal
         val template = Lib.typing_of_term major
         val types = filter (fn th => Term.could_unify (template, th)) (facts @ prems)
-- 
cgit v1.2.3