src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

     (string * stature) list
   val used_facts_in_unsound_atp_proof :
     Proof.context -> (string * stature) list vector -> 'a proof ->
     string list option
   val isar_proof_text :
-    Proof.context -> bool option -> isar_params -> one_line_params -> string
+    Proof.context -> bool -> bool option -> isar_params -> one_line_params -> string
   val proof_text :
-    Proof.context -> bool option -> isar_params -> int -> one_line_params
+    Proof.context -> bool -> bool option -> isar_params -> int -> one_line_params
     -> string
 end;
 
 structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
 struct

 type isar_params =
   bool * bool * Time.time option * bool * real * int * real * bool * bool
   * string Symtab.table * (string * stature) list vector
   * (string * term) list * int Symtab.table * string proof * thm
 
-fun isar_proof_text ctxt isar_proofs
+fun isar_proof_text ctxt auto 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)
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let

       params
       |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
       |> (fn fixes =>
              ctxt |> Variable.set_body false
                   |> Proof_Context.add_fixes fixes)
-    val one_line_proof = one_line_proof_text 0 one_line_params
+    val one_line_proof = one_line_proof_text auto 0 one_line_params
     val type_enc =
       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
       else partial_typesN
     val lam_trans = lam_trans_of_atp_proof atp_proof metis_default_lam_trans
     val do_preplay = preplay_timeout <> SOME Time.zeroTime

                else
                  [])
           in
             "\n\nStructured proof"
               ^ (commas msg |> not (null msg) ? enclose " (" ")")
-              ^ ":\n" ^ Active.sendback_markup isar_text
+              ^ ":\n" ^
+              Active.sendback_markup (if auto then [Markup.padding_command] else []) isar_text
           end
       end
     val isar_proof =
       if debug then
         isar_proof_of ()

   case preplay of
     Played (reconstr, _) => reconstr = SMT
   | Trust_Playable _ => true
   | Failed_to_Play _ => true
 
-fun proof_text ctxt isar_proofs isar_params num_chained
+fun proof_text ctxt auto 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 isar_proofs isar_params
+     isar_proof_text ctxt auto isar_proofs isar_params
    else
-     one_line_proof_text num_chained) one_line_params
+     one_line_proof_text auto num_chained) one_line_params
 
 end;