src/FOL/IFOL.thy

   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   and [Pure.elim 2] = allE notE' impE'
   and [Pure.intro] = exI disjI2 disjI1
 
 ML_setup {*
-  Context.>> (RuleContext.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac));
+  Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac));
 *}
 
 
 subsection {* Atomizing meta-level rules *}