--- a/src/ZF/UNITY/SubstAx.thy Thu Jul 02 17:33:36 2009 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Thu Jul 02 17:34:14 2009 +0200
@@ -359,7 +359,7 @@
REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
- simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2,
+ simp_tac (ss addsimps (Program_Defs.get ctxt)) 2,
res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ss addsimps [@{thm domain_def}]) 3,