# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 7a2bc89ac48e41dacb09b5a095a75b176c3491d1
# Parent  c71657bbdbc0bb82d32e5108bd8856e751276620
whitespace tuning

diff -r c71657bbdbc0 -r 7a2bc89ac48e src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -839,8 +839,7 @@
         #>> mk_aquant q [(`make_bound_var s, SOME T)]
       end
     and do_conn bs c t1 t2 =
-      do_formula bs t1 ##>> do_formula bs t2
-      #>> uncurry (mk_aconn c)
+      do_formula bs t1 ##>> do_formula bs t2 #>> uncurry (mk_aconn c)
     and do_formula bs t =
       case t of
         @{const Trueprop} $ t1 => do_formula bs t1