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/ZF/Tools/inductive_package.ML
changeset 82695 d93ead9ac6df
parent 80636 4041e7c8059d 
--- a/src/ZF/Tools/inductive_package.ML	Thu Jun 12 08:03:05 2025 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Jun 12 12:44:47 2025 +0200
@@ -341,9 +341,9 @@
      (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
        If the premises get simplified, then the proofs could fail.*)
      val min_ss =
-           (empty_simpset ctxt4
-             |> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt))
-           setSolver (mk_solver "minimal"
+           empty_simpset ctxt4
+           |> Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)
+           |> Simplifier.set_unsafe_solver (mk_solver "minimal"
                       (fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt)
                                    ORELSE' assume_tac ctxt
                                    ORELSE' eresolve_tac ctxt @{thms FalseE}));
isabelle