src/ZF/UNITY/SubstAx.thy

                 ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
                 REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
                                   @{thm EnsuresI}, @{thm ensuresI}] 1),
             (*now there are two subgoals: co & transient*)
             simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2,
-            res_inst_tac ctxt [((("act", 0), Position.none), sact)] @{thm transientI} 2,
+            Rule_Insts.res_inst_tac ctxt [((("act", 0), Position.none), sact)] @{thm transientI} 2,
                (*simplify the command's domain*)
             simp_tac (ctxt addsimps [@{thm domain_def}]) 3,
             (* proving the domain part *)
            clarify_tac ctxt 3, dtac @{thm swap} 3, force_tac ctxt 4,
            rtac @{thm ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4,