# HG changeset patch
# User blanchet
# Date 1391418858 -3600
# Node ID e1bf9f0c54202a79070e2e1e9a7c0960bbaae438
# Parent  b84867d6550bf0cdedbbac29d354965b6d81b45b
less aggressive evaluation

diff -r b84867d6550b -r e1bf9f0c5420 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -314,7 +314,6 @@
           |> tap (trace_isar_proof "Original")
           |> compress_isar_proof ctxt compress_isar preplay_data
           |> tap (trace_isar_proof "Compressed")
-          |> tap (trace_isar_proof "Tried0")
           |> postprocess_isar_proof_remove_unreferenced_steps
                (keep_fastest_method_of_isar_step (!preplay_data)
                 #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
diff -r b84867d6550b -r e1bf9f0c5420 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -184,17 +184,24 @@
 
 fun peek_at_outcome outcome = if Lazy.is_finished outcome then Lazy.force outcome else Not_Played
 
+fun get_best_method_outcome force =
+  tap (List.app (K () o Lazy.future Future.default_params o snd)) (* optional parallelism *)
+  #> map (apsnd force)
+  #> sort (play_outcome_ord o pairself snd)
+  #> hd
+
 fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l =
   let
-    fun get_best_outcome_available get_one =
-      the (Canonical_Label_Tab.lookup preplay_data l)
-      |> map (apsnd get_one)
-      |> sort (play_outcome_ord o pairself snd)
-      |> hd |> snd
+    val meths_outcomes as (meth1, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l)
   in
-    (case get_best_outcome_available peek_at_outcome of
-      Not_Played => get_best_outcome_available Lazy.force
-    | outcome => outcome)
+    if forall (not o Lazy.is_finished o snd) meths_outcomes then
+      (case Lazy.force outcome1 of
+        outcome as Played _ => outcome
+      | _ => snd (get_best_method_outcome Lazy.force meths_outcomes))
+    else
+      (case get_best_method_outcome peek_at_outcome meths_outcomes of
+        (_, Not_Played) => snd (get_best_method_outcome Lazy.force meths_outcomes)
+      | (_, outcome) => outcome)
   end
 
 fun preplay_outcome_of_isar_step_for_method preplay_data l =
@@ -202,10 +209,8 @@
 
 fun fastest_method_of_isar_step preplay_data =
   the o Canonical_Label_Tab.lookup preplay_data
-  #> tap (List.app (K () o Lazy.future Future.default_params o snd)) (* optional parallelism *)
-  #> map (apsnd Lazy.force)
-  #> sort (play_outcome_ord o pairself snd)
-  #> hd #> fst
+  #> get_best_method_outcome Lazy.force
+  #> fst
 
 fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, (_, meths))) =
     Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths))