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/smt_normalize.ML
changeset 82967 73af47bc277c
parent 82643 f1c14af17591 
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Thu Aug 07 21:40:03 2025 +0200
@@ -429,7 +429,8 @@
   fun is_strange_number ctxt t = is_irregular_number t andalso SMT_Builtin.is_builtin_num ctxt t
 
   val proper_num_ss =
-    simpset_of (put_simpset HOL_ss \<^context> addsimps @{thms Num.numeral_One minus_zero})
+    simpset_of (put_simpset HOL_ss \<^context>
+      |> Simplifier.add_simps @{thms Num.numeral_One minus_zero})
 
   fun norm_num_conv ctxt =
     SMT_Util.if_conv (is_strange_number ctxt) (Simplifier.rewrite (put_simpset proper_num_ss ctxt))
isabelle