more Sledgehammer spying -- record fact indices

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Oct 04 14:35:00 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Oct 04 16:11:19 2013 +0200
@@ -73,7 +73,7 @@
     val ctxt = Proof.context_of state
 
     val hard_timeout = time_mult 3.0 (timeout |> the_default one_day)
-    val _ = spying spy (fn () => (state, subgoal, name, "launched"));
+    val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, hard_timeout)
     val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt slice name)
@@ -100,13 +100,21 @@
                   " proof (of " ^ string_of_int (length facts) ^ "): ") "."
       |> Output.urgent_message
 
-    fun spying_str_of_res ({outcome = NONE, used_facts, ...} : prover_result) =
-        let val num_used_facts = length used_facts in
+    fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
+        let
+          val num_used_facts = length used_facts
+          val indices =
+            tag_list 1 used_from
+            |> map (fn (j, fact) => fact |> apsnd (K j))
+            |> filter_used_facts false used_facts
+            |> map (prefix "@" o string_of_int o snd)
+        in
           "success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^
-          plural_s num_used_facts
+          plural_s num_used_facts ^
+          (if num_used_facts = 0 then "" else " (" ^ commas indices ^ ")")
         end
       | spying_str_of_res {outcome = SOME failure, ...} =
-        "failure: " ^ string_of_atp_failure failure
+        "Failure: " ^ string_of_atp_failure failure
 
     fun really_go () =
       problem
@@ -226,7 +234,7 @@
               | NONE => ()
       val _ = print "Sledgehammering..."
       val _ =
-        spying spy (fn () => (state, i, "***", "starting " ^ @{make_string} mode ^ " mode"))
+        spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode"))
       val (smts, (ueq_atps, full_atps)) =
         provers |> List.partition (is_smt_prover ctxt)
                 ||> List.partition (is_unit_equational_atp ctxt)
@@ -250,8 +258,7 @@
           |> (case is_appropriate_prop of
                 SOME is_app => filter (is_app o prop_of o snd)
               | NONE => I)
-          |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
-                            hyp_ts concl_t
+          |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
           |> tap (fn factss =>
                      if verbose then
                        label ^ plural_s (length provers) ^ ": " ^
@@ -259,9 +266,8 @@
                        |> print
                      else
                        ())
-          |> spy ? tap (fn factss =>
-            spying spy (fn () =>
-              (state, i, label ^ "s", "selected facts: " ^ spying_str_of_factss factss)))
+          |> spy ? tap (fn factss => spying spy (fn () =>
+            (state, i, label ^ "s", "Selected facts: " ^ spying_str_of_factss factss)))
         end
 
       fun launch_provers state label is_appropriate_prop provers =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Oct 04 14:35:00 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Oct 04 16:11:19 2013 +0200
@@ -162,7 +162,7 @@
 fun hackish_string_of_term ctxt =
   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
 
-val spying_version = "b"
+val spying_version = "c"
 
 fun spying false _ = ()
   | spying true f =