src/HOL/UNITY/UNITY_tactics.ML
changeset 27239 f2f42f9fa09d
parent 27208 5fe899199f85
child 30610 bcbc34cb9749
     1.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Mon Jun 16 17:56:08 2008 +0200
     1.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Mon Jun 16 22:13:39 2008 +0200
     1.3 @@ -41,9 +41,9 @@
     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 -              RuleInsts.res_inst_tac (Simplifier.the_context ss)
     1.8 +              res_inst_tac (Simplifier.the_context ss)
     1.9                  [(("act", 0), sact)] @{thm totalize_transientI} 2
    1.10 -              ORELSE RuleInsts.res_inst_tac (Simplifier.the_context ss)
    1.11 +              ORELSE 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,