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/Function/lexicographic_order.ML
changeset 82967 73af47bc277c
parent 82590 d08f5b5ead0a 
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Aug 07 21:40:03 2025 +0200
@@ -207,7 +207,7 @@
 fun lexicographic_order_tac quiet ctxt =
   TRY (Function_Common.termination_rule_tac ctxt 1) THEN
   lex_order_tac quiet ctxt
-    (auto_tac (ctxt addsimps (Named_Theorems.get ctxt \<^named_theorems>\<open>termination_simp\<close>)))
+    (auto_tac (ctxt |> Simplifier.add_simps (Named_Theorems.get ctxt \<^named_theorems>\<open>termination_simp\<close>)))
 
 val _ =
   Theory.setup
isabelle