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/Import/proof_kernel.ML
changeset 36543 0e7fc5bf38de
parent 35994 9cc3df9a606e
child 36610 bafd82950e24 
--- a/src/HOL/Import/proof_kernel.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -1249,7 +1249,7 @@
     let
         val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
         val hol4ss = Simplifier.global_context thy empty_ss
-          setmksimps single addsimps hol4rews1
+          setmksimps (K single) addsimps hol4rews1
     in
         Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
     end
isabelle