src/HOL/UNITY/UNITY_tactics.ML

     (EVERY
      [REPEAT (Always_Int_tac ctxt 1),
       (*reduce the fancy safety properties to "constrains"*)
       REPEAT (etac @{thm Always_ConstrainsI} 1
               ORELSE
-              resolve_tac [@{thm StableI}, @{thm stableI},
+              resolve_tac ctxt [@{thm StableI}, @{thm stableI},
                            @{thm constrains_imp_Constrains}] 1),
       (*for safety, the totalize operator can be ignored*)
       simp_tac (put_simpset HOL_ss ctxt
         addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1,
       rtac @{thm constrainsI} 1,