# HG changeset patch
# User blanchet
# Date 1381329603 -7200
# Node ID 4e299e2c762d52082b2c89037e3a393de0c5bb49
# Parent  1e2585f56509b28b60c49eb22451cf5a13a057cc
no isar proofs if preplay was not attempted

diff -r 1e2585f56509 -r 4e299e2c762d src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 09 16:38:48 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 09 16:40:03 2013 +0200
@@ -640,7 +640,7 @@
 fun isar_proof_would_be_a_good_idea preplay =
   case preplay of
     Played (reconstr, _) => reconstr = SMT
-  | Trust_Playable _ => true
+  | Trust_Playable _ => false
   | Failed_to_Play _ => true
 
 fun proof_text ctxt isar_proofs isar_params num_chained