# HG changeset patch
# User blanchet
# Date 1337079975 -7200
# Node ID c6d5418ee7708aa68cad58a76f1aafa4bbe6effa
# Parent  481e5379c4efedeec7f462c8491729008e0fbe82
fixed Waldmeister commutativity hack

diff -r 481e5379c4ef -r c6d5418ee770 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 15 13:06:15 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue May 15 13:06:15 2012 +0200
@@ -347,8 +347,9 @@
   | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
     c1 = c2 andalso length phis1 = length phis2 andalso
     forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2)
-  | is_same_formula comm subst (AAtom (ATerm ("equal", [tm11, tm12]))) (AAtom tm2) =
-    is_same_term subst (ATerm ("equal", [tm11, tm12])) tm2 orelse
+  | is_same_formula comm subst (AAtom (tm1 as ATerm ("equal", [tm11, tm12])))
+                    (AAtom tm2) =
+    is_same_term subst tm1 tm2 orelse
     (comm andalso is_same_term subst (ATerm ("equal", [tm12, tm11])) tm2)
   | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
   | is_same_formula _ _ _ _ = false
@@ -385,7 +386,7 @@
                         equation to avoid confusing Isar. *)
                      [(s, phi')] =>
                      ((num, [s]),
-                      phi |> not (is_same_formula false [] phi phi')
+                      phi |> not (is_same_formula false [] (mk_anot phi) phi')
                              ? commute_eq)
                    | _ => ((num, []), phi)
                  else