# HG changeset patch
# User blanchet
# Date 1466160018 -7200
# Node ID 540cfb14a751fa4184fc4cd6a8cc22373a24bfca
# Parent  caaacf37943f8ad9ce2ce5a78cd5baf148487a8c
be more careful before filtering out chained facts in Sledgehammer

diff -r caaacf37943f -r 540cfb14a751 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jun 17 12:37:43 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jun 17 12:40:18 2016 +0200
@@ -63,49 +63,51 @@
 fun is_metis_method (Metis_Method _) = true
   | is_metis_method _ = false
 
-fun play_one_line_proof minimize timeout used_facts0 state i (preferred_meth, methss) =
-  let val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts0 in
-    if timeout = Time.zeroTime then
-      (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
-    else
-      let
-        val ctxt = Proof.context_of state
+fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) =
+  (if timeout = Time.zeroTime then
+     (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
+   else
+     let
+       val ctxt = Proof.context_of state
 
-        val fact_names = map fst used_facts
-        val {facts = chained, goal, ...} = Proof.goal state
-        val goal_t = Logic.get_goal (Thm.prop_of goal) i
+       val fact_names = map fst used_facts
+       val {facts = chained, goal, ...} = Proof.goal state
+       val goal_t = Logic.get_goal (Thm.prop_of goal) i
 
-        fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
-          | try_methss ress [] =
-            (used_facts,
-             (case AList.lookup (op =) ress preferred_meth of
-               SOME play => (preferred_meth, play)
-             | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress))))
-          | try_methss ress (meths :: methss) =
-            let
-              fun mk_step fact_names meths =
-                Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
-            in
-              (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of
-                (res as (meth, Played time)) :: _ =>
-                (* if a fact is needed by an ATP, it will be needed by "metis" *)
-                if not minimize orelse is_metis_method meth then
-                  (used_facts, res)
-                else
-                  let
-                    val (time', used_names') =
-                      minimized_isar_step ctxt chained time (mk_step fact_names [meth])
-                      ||> (facts_of_isar_step #> snd)
-                    val used_facts' = filter (member (op =) used_names' o fst) used_facts
-                  in
-                    (used_facts', (meth, Played time'))
-                  end
-              | ress' => try_methss (ress' @ ress) methss)
-            end
-      in
-        try_methss [] methss
-      end
-  end
+       fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
+         | try_methss ress [] =
+           (used_facts,
+            (case AList.lookup (op =) ress preferred_meth of
+              SOME play => (preferred_meth, play)
+            | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress))))
+         | try_methss ress (meths :: methss) =
+           let
+             fun mk_step fact_names meths =
+               Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
+           in
+             (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of
+               (res as (meth, Played time)) :: _ =>
+               (* if a fact is needed by an ATP, it will be needed by "metis" *)
+               if not minimize orelse is_metis_method meth then
+                 (used_facts, res)
+               else
+                 let
+                   val (time', used_names') =
+                     minimized_isar_step ctxt chained time (mk_step fact_names [meth])
+                     ||> (facts_of_isar_step #> snd)
+                   val used_facts' = filter (member (op =) used_names' o fst) used_facts
+                 in
+                   (used_facts', (meth, Played time'))
+                 end
+             | ress' => try_methss (ress' @ ress) methss)
+           end
+     in
+       try_methss [] methss
+     end)
+  |> (fn (used_facts, (meth, play)) =>
+        (used_facts |> not (proof_method_distinguishes_chained_and_direct meth)
+           ? filter_out (fn (_, (sc, _)) => sc = Chained),
+         (meth, play)))
 
 fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout,
       expect, ...}) mode writeln_result only learn