# HG changeset patch
# User blanchet
# Date 1407149568 -7200
# Node ID 563df8185d981546ad2d5615598ed0aa17772b76
# Parent  1111a9a328fe92d8d91aae232b1639efd77c575b
more informative preplay failures

diff -r 1111a9a328fe -r 563df8185d98 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 04 12:28:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 04 12:52:48 2014 +0200
@@ -84,8 +84,9 @@
         val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
         val goal_t = Logic.list_implies (map prop_of chained @ hyp_ts, concl_t)
 
-        fun try_methss [] = dont_know ()
-          | try_methss (meths :: methss) =
+        fun try_methss [] [] = dont_know ()
+          | try_methss ress [] = (used_facts, hd (sort (play_outcome_ord o pairself snd) ress))
+          | try_methss ress (meths :: methss) =
             let
               fun mk_step fact_names meths =
                 Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
@@ -104,10 +105,10 @@
                   in
                     (used_facts', (meth, Played time'))
                   end
-              | _ => try_methss methss)
+              | ress' => try_methss (ress' @ ress) methss)
             end
       in
-        try_methss methss
+        try_methss [] methss
       end
   end
 
diff -r 1111a9a328fe -r 563df8185d98 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Aug 04 12:28:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Aug 04 12:52:48 2014 +0200
@@ -179,13 +179,9 @@
     (s |> s <> "" ? enclose " (" ")") ^ "."
   end
 
-fun split_used_facts facts =
-  facts
-  |> List.partition (fn (_, (sc, _)) => sc = Chained)
-
 fun one_line_proof_text ctxt num_chained
     ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
-  let val (chained, extra) = split_used_facts used_facts in
+  let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in
     map fst extra
     |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
     |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "."