# HG changeset patch
# User blanchet
# Date 1407150384 -7200
# Node ID cf4215911f851eef555fa6e3a036eff0f51f9b33
# Parent  563df8185d981546ad2d5615598ed0aa17772b76
default on 'metis' for ATPs if preplaying is disabled

diff -r 563df8185d98 -r cf4215911f85 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 04 12:52:48 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 04 13:06:24 2014 +0200
@@ -66,51 +66,46 @@
 fun is_metis_method (Metis_Method _) = true
   | is_metis_method _ = false
 
-fun play_one_line_proof minimize timeout used_facts state i
-    (preferred, methss as (meth :: _) :: _) =
-  let
-    fun dont_know () =
-      (used_facts,
-       (if exists (fn meths => member (op =) meths preferred) methss then preferred else meth,
-        Play_Timed_Out Time.zeroTime))
-  in
-    if timeout = Time.zeroTime then
-      dont_know ()
-    else
-      let
-        val fact_names = map fst used_facts
+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 fact_names = map fst used_facts
 
-        val {context = ctxt, facts = chained, goal} = Proof.goal state
-        val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
-        val goal_t = Logic.list_implies (map prop_of chained @ hyp_ts, concl_t)
+      val {context = ctxt, facts = chained, goal} = Proof.goal state
+      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 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, "")
-            in
-              (case preplay_isar_step ctxt 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 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 ress [] =
+          (used_facts,
+           (case AList.lookup (op =) ress preferred_meth of
+             SOME play => (preferred_meth, play)
+           | NONE => hd (sort (play_outcome_ord o pairself 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 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 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
 
 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout,
       preplay_timeout, expect, ...}) mode output_result only learn
diff -r 563df8185d98 -r cf4215911f85 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Aug 04 12:52:48 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Aug 04 13:06:24 2014 +0200
@@ -362,9 +362,9 @@
           val used_facts = sort_wrt fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof)
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
           val preferred_methss =
-            bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types
-              (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
-            |> `(hd o hd)
+            (Metis_Method (NONE, NONE),
+             bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types
+               (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN))
         in
           (used_facts, preferred_methss,
            fn preplay =>