src/HOL/UNITY/UNITY_tactics.ML
changeset 27208 5fe899199f85
parent 24147 edc90be09ac1
child 27239 f2f42f9fa09d
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Sat Jun 14 17:49:24 2008 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Sat Jun 14 23:19:51 2008 +0200
     1.3 @@ -41,8 +41,10 @@
     1.4                                      @{thm EnsuresI}, @{thm ensuresI}] 1),
     1.5                (*now there are two subgoals: co & transient*)
     1.6                simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2,
     1.7 -              res_inst_tac [("act", sact)] @{thm totalize_transientI} 2
     1.8 -              ORELSE res_inst_tac [("act", sact)] @{thm transientI} 2,
     1.9 +              RuleInsts.res_inst_tac (Simplifier.the_context ss)
    1.10 +                [(("act", 0), sact)] @{thm totalize_transientI} 2
    1.11 +              ORELSE RuleInsts.res_inst_tac (Simplifier.the_context ss)
    1.12 +                [(("act", 0), sact)] @{thm transientI} 2,
    1.13                   (*simplify the command's domain*)
    1.14                simp_tac (ss addsimps [@{thm Domain_def}]) 3,
    1.15                constrains_tac (cs,ss) 1,