# HG changeset patch
# User blanchet
# Date 1376380688 -7200
# Node ID fcd3a59c6f7289447178f7e763d2062cdd49fe9e
# Parent  dd28fbc5cecb5617fefd298927559210902913a2
whitepsace tuning

diff -r dd28fbc5cecb -r fcd3a59c6f72 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Tue Aug 13 09:57:55 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Tue Aug 13 09:58:08 2013 +0200
@@ -82,7 +82,8 @@
       "" => ""
     | command =>
       "\nTo minimize: " ^
-      Active.sendback_markup (if auto then [Markup.padding_command] else []) command ^ "."
+      Active.sendback_markup (if auto then [Markup.padding_command] else [])
+                             command ^ "."
 
 fun split_used_facts facts =
   facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
@@ -124,7 +125,6 @@
 
 fun string_of_proof ctxt type_enc lam_trans i n proof =
   let
-
     val ctxt =
       (* make sure type constraint are actually printed *)
       ctxt |> Config.put show_markup false
@@ -147,7 +147,7 @@
     fun of_obtain qs nr =
       (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
          "ultimately "
-       else if nr=1 orelse member (op =) qs Then then
+       else if nr = 1 orelse member (op =) qs Then then
          "then "
        else
          "") ^ "obtain"