generate Isar proof if Metis appears to be too slow

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 21 12:22:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Feb 21 12:22:26 2013 +0100
@@ -936,7 +936,7 @@
               let
                 val _ =
                   if verbose then
-                    Output.urgent_message "Generating proof text..."
+                    Output.urgent_message "Generating structured proof..."
                   else
                     ()
                 val isar_params =

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