1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 21 12:22:26 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 21 12:22:26 2013 +0100
     1.3 @@ -936,7 +936,7 @@
     1.4                let
     1.5                  val _ =
     1.6                    if verbose then
     1.7 -                    Output.urgent_message "Generating proof text..."
     1.8 +                    Output.urgent_message "Generating structured proof..."
     1.9                    else
    1.10                      ()
    1.11                  val isar_params =

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Feb 21 12:22:26 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Feb 21 12:22:26 2013 +0100
     2.3 @@ -839,7 +839,7 @@
     2.4  fun isar_proof_would_be_a_good_idea preplay =
     2.5    case preplay of
     2.6      Played (reconstr, _) => reconstr = SMT
     2.7 -  | Trust_Playable _ => false
     2.8 +  | Trust_Playable _ => true
     2.9    | Failed_to_Play _ => true
    2.10  
    2.11  fun proof_text ctxt isar_proofs isar_params num_chained