src/ZF/UNITY/SubstAx.thy
changeset 31902 862ae16a799d
parent 30549 d2d7874648bd
child 32149 ef59550a55d3
     1.1 --- a/src/ZF/UNITY/SubstAx.thy	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/ZF/UNITY/SubstAx.thy	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -359,7 +359,7 @@
     1.4                    REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
     1.5                                      @{thm EnsuresI}, @{thm ensuresI}] 1),
     1.6                (*now there are two subgoals: co & transient*)
     1.7 -              simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
     1.8 +              simp_tac (ss addsimps (Program_Defs.get ctxt)) 2,
     1.9                res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
    1.10                   (*simplify the command's domain*)
    1.11                simp_tac (ss addsimps [@{thm domain_def}]) 3,