diff -r bdf9a78d46cf -r 9ae5c21fc88c src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sat Mar 03 23:49:22 2012 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Sat Mar 03 23:49:54 2012 +0100
@@ -1114,8 +1114,8 @@
 
 fun rewrite_hol4_term t thy =
     let
-        val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
-        val hol4ss = Simplifier.global_context thy empty_ss addsimps hol4rews1
+        val import_rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
+        val hol4ss = Simplifier.global_context thy empty_ss addsimps import_rews1
     in
         Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
     end