# HG changeset patch
# User blanchet
# Date 1391467479 -3600
# Node ID 455a7f9924dfe96a1bed09cfcb2545f055cdb109
# Parent  dc68f6fb88d291e00136d6a6c0391cf31ac60904
don't lose additional outcomes

diff -r dc68f6fb88d2 -r 455a7f9924df src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 23:38:33 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 23:44:39 2014 +0100
@@ -152,13 +152,15 @@
         end
 
       (* elimination of trivial, one-step subproofs *)
-      fun elim_one_subproof time qs fix l t lfs gfs (meths as meth :: _) comment subs nontriv_subs =
+      fun elim_one_subproof time meths_outcomes qs fix l t lfs gfs (meths as meth :: _) comment subs
+          nontriv_subs =
         if null subs orelse not (compress_further ()) then
           let
             val subproofs = List.revAppend (nontriv_subs, subs)
             val step = Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)
           in
-            set_preplay_outcomes_of_isar_step ctxt time preplay_data step [(meth, Played time)];
+            set_preplay_outcomes_of_isar_step ctxt time preplay_data step
+              ((meth, Played time) :: meths_outcomes);
             step
           end
         else
@@ -180,14 +182,15 @@
 
               (* check if the modified step can be preplayed fast enough *)
               val timeout = slackify_merge_timeout (Time.+ (time, time'))
-              val outcomes as (_, Played time'') :: _ = preplay_isar_step ctxt timeout step''
+              val (_, Played time'') :: meths_outcomes = preplay_isar_step ctxt timeout step''
             in
               decrement_step_count (); (* l' successfully eliminated! *)
               map (replace_successor l' [l]) lfs';
-              elim_one_subproof time'' qs fix l t lfs'' gfs'' meths comment subs nontriv_subs
+              elim_one_subproof time'' meths_outcomes qs fix l t lfs'' gfs'' meths comment subs
+                nontriv_subs
             end
             handle Bind =>
-              elim_one_subproof time qs fix l t lfs gfs meths comment subs (sub :: nontriv_subs))
+              elim_one_subproof time [] qs fix l t lfs gfs meths comment subs (sub :: nontriv_subs))
           | _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof")
 
       fun elim_subproofs (step as Prove (qs, fix, l, t, subproofs, (lfs, gfs), meths, comment)) =
@@ -195,7 +198,7 @@
             step
           else
             (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of
-              Played time => elim_one_subproof time qs fix l t lfs gfs meths comment subproofs []
+              Played time => elim_one_subproof time [] qs fix l t lfs gfs meths comment subproofs []
             | _ => step)
         | elim_subproofs step = step
 
diff -r dc68f6fb88d2 -r 455a7f9924df src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 23:38:33 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 23:44:39 2014 +0100
@@ -187,7 +187,7 @@
 
 fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l =
   let
-    val meths_outcomes as (meth1, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l)
+    val meths_outcomes as (_, outcome1) :: _ = the (Canonical_Label_Tab.lookup preplay_data l)
   in
     if forall (not o Lazy.is_finished o snd) meths_outcomes then
       (case Lazy.force outcome1 of
diff -r dc68f6fb88d2 -r 455a7f9924df src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 23:38:33 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 23:44:39 2014 +0100
@@ -191,7 +191,7 @@
           (accum as (_, subst)) =
         let
           val lfs' = maps (the_list o AList.lookup (op =) subst) lfs
-          val (l', accum' as (next', subst')) = next_label depth have_prefix l accum
+          val (l', accum' as (_, subst')) = next_label depth have_prefix l accum
           val subs' = map (relabel_proof subst' (depth + 1)) subs
         in
           (Prove (qs, xs, l', t, subs', (lfs', gfs), meths, comment), accum')
@@ -305,7 +305,7 @@
     and add_step ind (Let (t1, t2)) =
         add_str (of_indent ind ^ "let ")
         #> add_term t1 #> add_str " = " #> add_term t2 #> add_str "\n"
-      | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meths as meth :: _, comment)) =
+      | add_step ind (Prove (qs, xs, l, t, subs, (ls, ss), meth :: _, comment)) =
         add_step_pre ind qs subs
         #> (case xs of
              [] => add_str (of_have qs (length subs) ^ " ")