src/HOL/Statespace/state_space.ML

   (case goal of
     Const (@{const_name Trueprop}, _) $
       (Const (@{const_name Not}, _) $
         (Const (@{const_name HOL.eq}, _) $ (x as Free _) $ (y as Free _))) =>
       (case neq_x_y ctxt x y of
-        SOME neq => rtac neq i
+        SOME neq => resolve_tac ctxt [neq] i
       | NONE => no_tac)
   | _ => no_tac));
 
 val distinctNameSolver = mk_solver "distinctNameSolver" distinctTree_tac;
 

   let
     fun solve_tac ctxt = CSUBGOAL (fn (goal, i) =>
       let
         val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name;
         val rule = DistinctTreeProver.distinct_implProver ctxt distinct_thm goal;
-      in rtac rule i end);
+      in resolve_tac ctxt [rule] i end);
 
     fun tac ctxt =
       Locale.intro_locales_tac true ctxt [] THEN ALLGOALS (solve_tac ctxt);
 
   in