diff -r cba2ddfb30c4 -r 8dceafa07c4f src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Aug 16 23:11:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sat Aug 17 11:34:50 2013 +0200
@@ -25,9 +25,9 @@
     Proof.context -> (string * stature) list vector -> 'a proof ->
     string list option
   val isar_proof_text :
-    Proof.context -> bool -> bool option -> isar_params -> one_line_params -> string
+    Proof.context -> Properties.T -> bool option -> isar_params -> one_line_params -> string
   val proof_text :
-    Proof.context -> bool -> bool option -> isar_params -> int -> one_line_params
+    Proof.context -> Properties.T -> bool option -> isar_params -> int -> one_line_params
     -> string
 end;
 
@@ -412,7 +412,7 @@
   * string Symtab.table * (string * stature) list vector
   * (string * term) list * int Symtab.table * string proof * thm
 
-fun isar_proof_text ctxt auto isar_proofs
+fun isar_proof_text ctxt sendback_props isar_proofs
     (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
      isar_compress_degree, merge_timeout_slack, isar_try0, isar_minimize, pool,
      fact_names, lifted, sym_tab, atp_proof, goal)
@@ -425,7 +425,7 @@
       |> (fn fixes =>
              ctxt |> Variable.set_body false
                   |> Proof_Context.add_fixes fixes)
-    val one_line_proof = one_line_proof_text auto 0 one_line_params
+    val one_line_proof = one_line_proof_text sendback_props 0 one_line_params
     val type_enc =
       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
       else partial_typesN
@@ -625,7 +625,7 @@
             "\n\nStructured proof"
               ^ (commas msg |> not (null msg) ? enclose " (" ")")
               ^ ":\n" ^
-              Active.sendback_markup (if auto then [Markup.padding_command] else []) isar_text
+              Active.sendback_markup sendback_props isar_text
           end
       end
     val isar_proof =
@@ -645,12 +645,12 @@
   | Trust_Playable _ => true
   | Failed_to_Play _ => true
 
-fun proof_text ctxt auto isar_proofs isar_params num_chained
+fun proof_text ctxt sendback_props isar_proofs isar_params num_chained
                (one_line_params as (preplay, _, _, _, _, _)) =
   (if isar_proofs = SOME true orelse
       (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
-     isar_proof_text ctxt auto isar_proofs isar_params
+     isar_proof_text ctxt sendback_props isar_proofs isar_params
    else
-     one_line_proof_text auto num_chained) one_line_params
+     one_line_proof_text sendback_props num_chained) one_line_params
 
 end;