simplified -- empty_ss already contains minimal mksimps;

--- a/src/HOL/Import/proof_kernel.ML	Thu Nov 24 19:58:37 2011 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Thu Nov 24 20:45:34 2011 +0100
@@ -1165,8 +1165,7 @@
 fun rewrite_hol4_term t thy =
     let
         val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
-        val hol4ss = Simplifier.global_context thy empty_ss
-          setmksimps (K single) addsimps hol4rews1
+        val hol4ss = Simplifier.global_context thy empty_ss addsimps hol4rews1
     in
         Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
     end

--- a/src/HOL/Import/shuffler.ML	Thu Nov 24 19:58:37 2011 +0100
+++ b/src/HOL/Import/shuffler.ML	Thu Nov 24 20:45:34 2011 +0100
@@ -467,7 +467,6 @@
     let
         val norms = ShuffleData.get thy
         val ss = Simplifier.global_context thy empty_ss
-          setmksimps (K single)
           addsimps (map (Thm.transfer thy) norms)
           addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
         fun chain f th =