--- 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