diff -r 4fb12e2598dc -r 9ee38fc0bc81 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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