aboutsummaryrefslogtreecommitdiff
path: root/spartan
diff options
context:
space:
mode:
Diffstat (limited to 'spartan')
-rw-r--r--spartan/core/types.ML4
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)