src/HOL/Tools/res_axioms.ML

 fun neg_clausify_tac ctxt =
   neg_skolemize_tac ctxt THEN'
   SUBGOAL (fn (prop, i) =>
     let val ts = Logic.strip_assums_hyp prop in
       EVERY'
-       [FOCUS
+       [Subgoal.FOCUS
          (fn {prems, ...} =>
            (Method.insert_tac
              (map forall_intr_vars (neg_clausify prems)) i)) ctxt,
         REPEAT_DETERM_N (length ts) o etac thin_rl] i
      end);