Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/proof_kernel.ML
changeset 35232 f588e1169c8b
parent 33339 d41f77196338
child 35390 efad0e364738 
--- a/src/HOL/Import/proof_kernel.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -1248,7 +1248,7 @@
 fun rewrite_hol4_term t thy =
     let
         val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
-        val hol4ss = Simplifier.theory_context thy empty_ss
+        val hol4ss = Simplifier.global_context thy empty_ss
           setmksimps single addsimps hol4rews1
     in
         Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t))
isabelle