Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/SMT/verit_replay.ML
changeset 82967 73af47bc277c
parent 82643 f1c14af17591 
--- a/src/HOL/Tools/SMT/verit_replay.ML	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/Tools/SMT/verit_replay.ML	Thu Aug 07 21:40:03 2025 +0200
@@ -74,7 +74,7 @@
         (Symtab.map (K rewrite) insts)
         decls
         (concl, ctxt)
-      |> Simplifier.simplify (empty_simpset ctxt addsimps rewrite_rules)
+      |> Simplifier.simplify (empty_simpset ctxt |> Simplifier.add_simps rewrite_rules)
   end
 
 fun add_used_asserts_in_step (Lethe_Proof.Lethe_Replay_Node {prems,
@@ -244,7 +244,7 @@
         proof_ctxt = [],
         concl = Thm.prop_of th
           |> Simplifier.rewrite_term (Proof_Context.theory_of
-               (empty_simpset ctxt addsimps rewrite_rules)) rewrite_rules [],
+               (empty_simpset ctxt |> Simplifier.add_simps rewrite_rules)) rewrite_rules [],
         bounds = [],
         insts = Symtab.empty,
         declarations = [],
isabelle