fixed Waldmeister commutativity hack
authorblanchet
Tue May 15 13:06:15 2012 +0200 (2012-05-15)
changeset 47926c6d5418ee770
parent 47925 481e5379c4ef
child 47927 c35238d19bb9
fixed Waldmeister commutativity hack
src/HOL/Tools/ATP/atp_proof.ML
     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