# HG changeset patch
# User wenzelm
# Date 1206567610 -3600
# Node ID 02709831944abbd32a6982d73df10b158b89a882
# Parent  af821e3a99e105ca8f7bbd643cc3e5a2830d4dca
removed legacy ML bindings;

diff -r af821e3a99e1 -r 02709831944a src/ZF/UNITY/SubstAx.thy
--- 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),