src/HOL/HOL.thy

   fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso
     Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false)
       (nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm;
 in
   Hypsubst.hypsubst_setup
-  #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+  #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
 end
 *}
 
 declare iffI [intro!]
   and notI [intro!]