# HG changeset patch
# User blanchet
# Date 1378930844 -7200
# Node ID 3d9f4ac93bcab07ad764dcc576cb185a173c6d48
# Parent  785b57a1ffe2827352b58247e06f49430a7ca29d
tuning

diff -r 785b57a1ffe2 -r 3d9f4ac93bca src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Sep 11 22:20:43 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Sep 11 22:20:44 2013 +0200
@@ -246,7 +246,8 @@
              factss = factss}
           fun learn prover =
             mash_learn_proof ctxt params prover (prop_of goal) all_facts
-          val launch = launch_prover params mode output_result minimize_command only learn
+          val launch =
+            launch_prover params mode output_result minimize_command only learn
         in
           if mode = Auto_Try then
             (unknownN, state)