# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID 25d498554c483ee456b8bf2792964ea355fce2d6
# Parent  b6af899a78ac92e57ee1b0bbc9899e2ff32704aa
further minimize one-liner

diff -r b6af899a78ac -r 25d498554c48 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -34,6 +34,7 @@
 open Sledgehammer_Proof_Methods
 open Sledgehammer_Isar_Proof
 open Sledgehammer_Isar_Preplay
+open Sledgehammer_Isar_Minimize
 open Sledgehammer_Prover
 open Sledgehammer_Prover_ATP
 open Sledgehammer_Prover_Minimize
@@ -78,9 +79,22 @@
 
         fun try_methss [] = dont_know ()
           | try_methss (meths :: methss) =
-            let val step = Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") in
-              (case preplay_isar_step ctxt timeout [] step of
-                (res as (_, Played _)) :: _ => (used_facts, res)
+            let
+              fun mk_step fact_names meths =
+                Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
+            in
+              (case preplay_isar_step ctxt timeout [] (mk_step fact_names meths) of
+                (res as (Metis_Method _, Played _)) :: _ =>
+                (used_facts, res) (* if a fact is needed by an ATP, it will be needed by "metis" *)
+              | (meth, Played time) :: _ =>
+                let
+                  val (time', used_names') =
+                    minimized_isar_step ctxt 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
               | _ => try_methss methss)
             end
       in