# HG changeset patch
# User blanchet
# Date 1402420514 -7200
# Node ID a582f98292c019b1b56a75e1f4aa35e59dfdbc19
# Parent  697e0fad93370ef1ad36e6fd28db663083a870ed
tuning

diff -r 697e0fad9337 -r a582f98292c0 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 10 18:24:53 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 10 19:15:14 2014 +0200
@@ -406,8 +406,7 @@
   | 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 (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) =
+  | is_same_formula comm subst (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) =
     is_same_term subst tm1 tm2 orelse
     (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2)
   | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
@@ -451,8 +450,8 @@
                 File_Source (_, SOME s) =>
                 (if s = waldmeister_conjecture_name then
                    (case find_formula_in_problem (mk_anot phi) problem of
-                     (* Waldmeister hack: Get the original orientation of the
-                        equation to avoid confusing Isar. *)
+                     (* Waldmeister hack: Get the original orientation of the equation to avoid
+                        confusing Isar. *)
                      [(s, phi')] =>
                      ((num, [s]),
                       phi |> not (is_same_formula false [] (mk_anot phi) phi') ? commute_eq)