--- 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,