--- a/src/ZF/UNITY/SubstAx.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Fri Mar 20 14:48:04 2015 +0100
@@ -359,7 +359,7 @@
@{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 *)