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 36543 0e7fc5bf38de
parent 36541 de1862c4a308
child 36546 a9873318fe30 
--- a/src/ZF/Tools/inductive_package.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -328,7 +328,7 @@
      (*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 = Simplifier.global_context thy empty_ss
-           setmksimps (map mk_eq o ZF_atomize o gen_all)
+           setmksimps (K (map mk_eq o ZF_atomize o gen_all))
            setSolver (mk_solver "minimal"
                       (fn prems => resolve_tac (triv_rls@prems)
                                    ORELSE' assume_tac
isabelle