--- a/src/ZF/UNITY/SubstAx.thy Wed Mar 26 22:40:09 2008 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Wed Mar 26 22:40:10 2008 +0100
@@ -364,7 +364,7 @@
(*simplify the command's domain*)
simp_tac (ss addsimps [@{thm domain_def}]) 3,
(* proving the domain part *)
- clarify_tac cs 3, dtac Cla.swap 3, force_tac css 4,
+ clarify_tac cs 3, dtac @{thm swap} 3, force_tac css 4,
rtac @{thm ReplaceI} 3, force_tac css 3, force_tac css 4,
asm_full_simp_tac ss 3, rtac conjI 3, simp_tac ss 4,
REPEAT (rtac @{thm state_update_type} 3),