src/Provers/Arith/fast_lin_arith.ML

           REPEAT_DETERM (eresolve_tac neqE i)
         else
           all_tac) THEN
           PRIMITIVE (trace_thm ctxt "State after neqE:") THEN
           (* use theorems generated from the actual justifications *)
-          FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i
+          Subgoal.FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i
     in
       (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
       DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
       (* user-defined preprocessing of the subgoal *)
       DETERM (LA_Data.pre_tac ctxt i) THEN