From 549f1d46884d068ebf18f76bb359624510b086b0 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 19 Jan 2021 02:18:44 +0000
Subject: Bugfix: no longer repeatedly add duplicate rules to simpset

---
 spartan/core/types.ML | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/spartan/core/types.ML b/spartan/core/types.ML
index 67918b9..5e0d484 100644
--- a/spartan/core/types.ML
+++ b/spartan/core/types.ML
@@ -99,7 +99,9 @@ and check_infer facts i (cst as (_, st)) =
 and compute_tac ctxt facts =
   let
     val comps = Named_Theorems.get ctxt \<^named_theorems>\<open>comp\<close>
-    val ctxt' = ctxt addsimps comps
+    val ss = simpset_of ctxt
+    val ss' = simpset_of (empty_simpset ctxt addsimps comps)
+    val ctxt' = put_simpset (merge_ss (ss, ss')) ctxt
   in
     SUBGOAL (fn (_, i) =>
       ((CHANGED o asm_simp_tac ctxt' ORELSE' EqSubst.eqsubst_tac ctxt [0] comps)
-- 
cgit v1.2.3