# HG changeset patch
# User blanchet
# Date 1350567675 -7200
# Node ID 073d69478207f6f5e8e4631bda76d5f3c613cb1a
# Parent  26a0263f9f4681ddc9a5ad20e9c35f396de72df7
tuned Isar output

diff -r 26a0263f9f46 -r 073d69478207 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Oct 18 15:40:02 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Oct 18 15:41:15 2012 +0200
@@ -882,6 +882,11 @@
               end,
            fn preplay =>
               let
+                val _ =
+                  if verbose then
+                    Output.urgent_message "Generating proof text..."
+                  else
+                    ()
                 val isar_params =
                   (debug, verbose, isar_shrinkage, pool, fact_names, sym_tab,
                    atp_proof, goal)
diff -r 26a0263f9f46 -r 073d69478207 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Oct 18 15:40:02 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Oct 18 15:41:15 2012 +0200
@@ -634,7 +634,8 @@
       maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
       o annotate_types ctxt
     val reconstr = Metis (type_enc, lam_trans)
-    fun do_facts (ls, ss) =
+    fun do_facts ind (ls, ss) =
+      "\n" ^ do_indent (ind + 1) ^
       reconstructor_command reconstr 1 1 [] 0
           (ls |> sort_distinct (prod_ord string_ord int_ord),
            ss |> sort_distinct string_ord)
@@ -646,12 +647,12 @@
         do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
       | do_step ind (Prove (qs, l, t, By_Metis facts)) =
         do_indent ind ^ do_have qs ^ " " ^
-        do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
+        do_label l ^ do_term t ^ do_facts ind facts ^ "\n"
       | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
         implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
                      proofs) ^
-        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
-        do_facts facts ^ "\n"
+        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^
+        do_facts ind facts ^ "\n"
     and do_steps prefix suffix ind steps =
       let val s = implode (map (do_step ind) steps) in
         replicate_string (ind * indent_size - size prefix) " " ^ prefix ^