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 ^