author blanchet Tue May 15 13:06:15 2012 +0200 (2012-05-15) changeset 47926 c6d5418ee770 parent 47925 481e5379c4ef child 47927 c35238d19bb9
fixed Waldmeister commutativity hack
```     1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Tue May 15 13:06:15 2012 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue May 15 13:06:15 2012 +0200
1.3 @@ -347,8 +347,9 @@
1.4    | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
1.5      c1 = c2 andalso length phis1 = length phis2 andalso
1.6      forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2)
1.7 -  | is_same_formula comm subst (AAtom (ATerm ("equal", [tm11, tm12]))) (AAtom tm2) =
1.8 -    is_same_term subst (ATerm ("equal", [tm11, tm12])) tm2 orelse
1.9 +  | is_same_formula comm subst (AAtom (tm1 as ATerm ("equal", [tm11, tm12])))
1.10 +                    (AAtom tm2) =
1.11 +    is_same_term subst tm1 tm2 orelse
1.12      (comm andalso is_same_term subst (ATerm ("equal", [tm12, tm11])) tm2)
1.13    | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
1.14    | is_same_formula _ _ _ _ = false
1.15 @@ -385,7 +386,7 @@
1.16                          equation to avoid confusing Isar. *)
1.17                       [(s, phi')] =>
1.18                       ((num, [s]),
1.19 -                      phi |> not (is_same_formula false [] phi phi')
1.20 +                      phi |> not (is_same_formula false [] (mk_anot phi) phi')
1.21                               ? commute_eq)
1.22                     | _ => ((num, []), phi)
1.23                   else
```