diff -r 548e2d3105b9 -r 5fe899199f85 src/HOL/UNITY/UNITY_tactics.ML
--- a/src/HOL/UNITY/UNITY_tactics.ML	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/UNITY/UNITY_tactics.ML	Sat Jun 14 23:19:51 2008 +0200
@@ -41,8 +41,10 @@
                                     @{thm EnsuresI}, @{thm ensuresI}] 1),
               (*now there are two subgoals: co & transient*)
               simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
-              res_inst_tac [("act", sact)] @{thm totalize_transientI} 2
-              ORELSE res_inst_tac [("act", sact)] @{thm transientI} 2,
+              RuleInsts.res_inst_tac (Simplifier.the_context ss)
+                [(("act", 0), sact)] @{thm totalize_transientI} 2
+              ORELSE RuleInsts.res_inst_tac (Simplifier.the_context ss)
+                [(("act", 0), sact)] @{thm transientI} 2,
                  (*simplify the command's domain*)
               simp_tac (ss addsimps [@{thm Domain_def}]) 3,
               constrains_tac (cs,ss) 1,