# HG changeset patch
# User wenzelm
# Date 1322163934 -3600
# Node ID 329bc52b4b8650498026b8424b27d4f2741d5e3e
# Parent  f682f3f7b726eec557e3c2eaf5a57ddf2d408dee
simplified -- empty_ss already contains minimal mksimps;

diff -r f682f3f7b726 -r 329bc52b4b86 src/HOL/Import/proof_kernel.ML
--- 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
diff -r f682f3f7b726 -r 329bc52b4b86 src/HOL/Import/shuffler.ML
--- 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 =