# HG changeset patch
# User blanchet
# Date 1381969374 -7200
# Node ID b4e6cd4cab92c1916fa4baeb0f467b6138add36d
# Parent  9ee9eee93c0685c4e69d6c138736caf7f897aca2
thread the goal through instead of relying on unreliable (possibly fake) state

diff -r 9ee9eee93c06 -r b4e6cd4cab92 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 17 01:34:34 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 17 02:22:54 2013 +0200
@@ -583,6 +583,7 @@
         ({pre=st, log, ...}: Mirabelle.run_args) =
   let
     val ctxt = Proof.context_of st
+    val {goal, ...} = Proof.goal st
     val n0 = length (these (!named_thms))
     val prover_name = get_prover_name ctxt args
     val type_enc = AList.lookup (op =) args type_encK |> the_default type_enc_default
@@ -612,7 +613,7 @@
           true 1 (Sledgehammer_Util.subgoal_count st)
     val _ = log separator
     val (used_facts, (preplay, message, message_tail)) =
-      minimize st NONE (these (!named_thms))
+      minimize st goal NONE (these (!named_thms))
     val msg = message (Lazy.force preplay) ^ message_tail
   in
     case used_facts of
diff -r 9ee9eee93c06 -r b4e6cd4cab92 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Oct 17 01:34:34 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Oct 17 02:22:54 2013 +0200
@@ -18,7 +18,7 @@
   val auto_minimize_max_time : real Config.T
   val minimize_facts :
     (string -> thm list -> unit) -> string -> params -> bool -> int -> int
-    -> Proof.state -> play Lazy.lazy option
+    -> Proof.state -> thm -> play Lazy.lazy option
     -> ((string * stature) * thm list) list
     -> ((string * stature) * thm list) list option
        * (play Lazy.lazy * (play -> string) * string)
@@ -59,7 +59,7 @@
                  max_new_mono_instances, type_enc, strict, lam_trans,
                  uncurried_aliases, isar_proofs, isar_compress, isar_try0,
                  preplay_timeout, ...} : params)
-               silent (prover : prover) timeout i n state facts =
+               silent (prover : prover) timeout i n state goal facts =
   let
     val _ =
       print silent (fn () =>
@@ -70,7 +70,6 @@
              | _ => ""
            else
              "") ^ "...")
-    val {goal, ...} = Proof.goal state
     val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
     val params =
       {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true,
@@ -191,12 +190,12 @@
   end
 
 fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
-                   i n state preplay0 facts =
+                   i n state goal preplay0 facts =
   let
     val ctxt = Proof.context_of state
     val prover =
       get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
-    fun test timeout = test_facts params silent prover timeout i n state
+    fun test timeout = test_facts params silent prover timeout i n state goal
     val (chained, non_chained) = List.partition is_fact_chained facts
     (* Push chained facts to the back, so that they are less likely to be
        kicked out by the linear minimization algorithm. *)
@@ -272,7 +271,7 @@
 
 fun maybe_minimize ctxt mode do_learn name
         (params as {verbose, isar_proofs, minimize, ...})
-        ({state, subgoal, subgoal_count, ...} : prover_problem)
+        ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
         (result as {outcome, used_facts, used_from, run_time, preplay, message,
                     message_tail} : prover_result) =
   if is_some outcome orelse null used_facts then
@@ -320,7 +319,7 @@
         if minimize then
           minimize_facts do_learn minimize_name params
               (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal
-              subgoal_count state (SOME preplay)
+              subgoal_count state goal (SOME preplay)
               (filter_used_facts true used_facts (map (apsnd single) used_from))
           |>> Option.map (map fst)
         else
@@ -342,12 +341,10 @@
 fun run_minimize (params as {provers, ...}) do_learn i refs state =
   let
     val ctxt = Proof.context_of state
+    val {goal, facts = chained_ths, ...} = Proof.goal state
     val reserved = reserved_isar_keyword_table ()
-    val chained_ths = #facts (Proof.goal state)
     val css = clasimpset_rule_table_of ctxt
-    val facts =
-      refs |> maps (map (apsnd single)
-                    o fact_of_ref ctxt reserved chained_ths css)
+    val facts = refs |> maps (map (apsnd single) o fact_of_ref ctxt reserved chained_ths css)
   in
     case subgoal_count state of
       0 => Output.urgent_message "No subgoal!"
@@ -355,7 +352,7 @@
              [] => error "No prover is set."
            | prover :: _ =>
              (kill_provers ();
-              minimize_facts do_learn prover params false i n state NONE facts
+              minimize_facts do_learn prover params false i n state goal NONE facts
               |> (fn (_, (preplay, message, message_tail)) =>
                      message (Lazy.force preplay) ^ message_tail
                      |> Output.urgent_message))