diff options
| author | Josh Chen | 2021-01-19 02:18:44 +0000 |
|---|---|---|
| committer | Josh Chen | 2021-01-19 02:18:44 +0000 |
| commit | 549f1d46884d068ebf18f76bb359624510b086b0 (patch) | |
| tree | b93746a4f947e8b9bd63cb53b945f8f0cc565e53 | |
| parent | f46df86db9308dde29e0e5f97f54546ea1dc34bf (diff) | |
Bugfix: no longer repeatedly add duplicate rules to simpset
| -rw-r--r-- | spartan/core/types.ML | 4 |
1 files changed, 3 insertions, 1 deletions
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) |