1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Apr 29 22:08:57 2010 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Apr 29 22:56:32 2010 +0200
     1.3 @@ -1249,7 +1249,7 @@
     1.4      let
     1.5          val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
     1.6          val hol4ss = Simplifier.global_context thy empty_ss
     1.7 -          setmksimps single addsimps hol4rews1
     1.8 +          setmksimps (K single) addsimps hol4rews1
     1.9      in
    1.10          Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
    1.11      end