# 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