diff -r 98e52f522357 -r f588e1169c8b src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Fri Feb 19 11:56:11 2010 +0100
+++ b/src/Provers/hypsubst.ML	Fri Feb 19 16:11:45 2010 +0100
@@ -156,7 +156,7 @@
     let fun tac i st = SUBGOAL (fn (Bi, _) =>
       let
         val (k, _) = eq_var bnd true Bi
-        val hyp_subst_ss = Simplifier.theory_context (Thm.theory_of_thm st) empty_ss
+        val hyp_subst_ss = Simplifier.global_context (Thm.theory_of_thm st) empty_ss
           setmksimps (mk_eqs bnd)
       in EVERY [rotate_tac k i, asm_lr_simp_tac hyp_subst_ss i,
         etac thin_rl i, rotate_tac (~k) i]