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/inductive.ML
changeset 82967 73af47bc277c
parent 82643 f1c14af17591 
--- a/src/HOL/Tools/inductive.ML	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Aug 07 21:40:03 2025 +0200
@@ -993,7 +993,7 @@
            fold_rev lambda params (fp_const $ fp_fun)))
       ||> Proof_Context.restore_naming lthy;
     val fp_def' =
-      Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
+      Simplifier.rewrite (put_simpset HOL_basic_ss lthy' |> Simplifier.add_simp fp_def)
         (Thm.cterm_of lthy' (list_comb (rec_const, params)));
     val specs =
       if is_auxiliary then
isabelle