1.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Feb 19 11:56:11 2010 +0100
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Feb 19 16:11:45 2010 +0100
     1.3 @@ -1248,7 +1248,7 @@
     1.4  fun rewrite_hol4_term t thy =
     1.5      let
     1.6          val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
     1.7 -        val hol4ss = Simplifier.theory_context thy empty_ss
     1.8 +        val hol4ss = Simplifier.global_context thy empty_ss
     1.9            setmksimps single addsimps hol4rews1
    1.10      in
    1.11          Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))