src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

   in one_line_proof ^ isar_proof end
 
 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
                (one_line_params as (preplay, _, _, _, _, _)) =
   (if isar_proofs = SOME true orelse