src/Provers/hypsubst.ML

     If bnd is true, then it replaces Bound variables only. *)
   fun gen_hyp_subst_tac bnd =
     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]
       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
     in REPEAT_DETERM1 o tac end;