--- a/src/ZF/UNITY/SubstAx.thy Thu Dec 08 20:15:34 2005 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Thu Dec 08 20:15:41 2005 +0100
@@ -416,7 +416,7 @@
(*simplify the command's domain*)
simp_tac (ss addsimps [domain_def]) 3,
(* proving the domain part *)
- clarify_tac cs 3, dtac swap 3, force_tac (cs,ss) 4,
+ clarify_tac cs 3, dtac Cla.swap 3, force_tac (cs,ss) 4,
rtac ReplaceI 3, force_tac (cs,ss) 3, force_tac (cs,ss) 4,
asm_full_simp_tac ss 3, rtac conjI 3, simp_tac ss 4,
REPEAT (rtac state_update_type 3),