# HG changeset patch
# User blanchet
# Date 1361445746 -3600
# Node ID 9ee38fc0bc811f4a4d120822c2daad2fa74f62e8
# Parent  4fb12e2598dc39bcb63cd2b8b82d0e60f133325b
generate Isar proof if Metis appears to be too slow

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