show index in fact list of all found facts

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Aug 30 11:49:29 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon Aug 30 12:02:51 2010 +0200
@@ -44,17 +44,19 @@
 
 fun done id ({log, ...} : Mirabelle.done_args) =
   if get id num_successes + get id num_failures > 0 then
-    (log ("\nNumber of overall success: " ^ Int.toString (get id num_successes));
-     log ("Number of overall failures: " ^ Int.toString (get id num_failures));
+    (log "";
+     log ("Number of overall successes: " ^
+          string_of_int (get id num_successes));
+     log ("Number of overall failures: " ^ string_of_int (get id num_failures));
      log ("Overall success rate: " ^
           percentage_alt (get id num_successes) (get id num_failures) ^ "%");
-     log ("Number of found proofs: " ^ Int.toString (get id num_found_proofs));
-     log ("Number of lost proofs: " ^ Int.toString (get id num_lost_proofs));
+     log ("Number of found proofs: " ^ string_of_int (get id num_found_proofs));
+     log ("Number of lost proofs: " ^ string_of_int (get id num_lost_proofs));
      log ("Proof found rate: " ^
           percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^
           "%");
-     log ("Number of found facts: " ^ Int.toString (get id num_found_facts));
-     log ("Number of lost facts: " ^ Int.toString (get id num_lost_facts));
+     log ("Number of found facts: " ^ string_of_int (get id num_found_facts));
+     log ("Number of lost facts: " ^ string_of_int (get id num_lost_facts));
      log ("Fact found rate: " ^
           percentage_alt (get id num_found_facts) (get id num_lost_facts) ^
           "%"))
@@ -63,6 +65,8 @@
 
 val default_max_relevant = 300
 
+fun with_index (i, s) = s ^ "@" ^ string_of_int i
+
 fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) =
   case (Position.line_of pos, Position.column_of pos) of
     (SOME line_num, SOME col_num) =>
@@ -84,7 +88,9 @@
            |> map (fst o fst)
          val (found_facts, lost_facts) =
            List.concat proofs |> sort_distinct string_ord
-           |> List.partition (member (op =) facts)
+           |> map (fn fact => (find_index (curry (op =) fact) facts, fact))
+           |> List.partition (curry (op <=) 0 o fst)
+           |>> sort (prod_ord int_ord string_ord) ||> map snd
          val found_proofs = filter (forall (member (op =) facts)) proofs
          val n = length found_proofs
          val _ =
@@ -93,13 +99,15 @@
            else
              (add id num_successes 1;
               add id num_found_proofs n;
-              log ("Success (" ^ Int.toString n ^ " of " ^
-                   Int.toString (length proofs) ^ " proofs)"))
+              log ("Success (" ^ string_of_int n ^ " of " ^
+                   string_of_int (length proofs) ^ " proofs)"))
          val _ = add id num_lost_proofs (length proofs - n)
          val _ = add id num_found_facts (length found_facts)
          val _ = add id num_lost_facts (length lost_facts)
-         val _ = if null found_facts then ()
-                 else log ("Found facts: " ^ commas found_facts)
+         val _ = if null found_facts then
+                   ()
+                 else
+                   log ("Found facts: " ^ commas (map with_index found_facts))
          val _ = if null lost_facts then ()
                  else log ("Lost facts: " ^ commas lost_facts)
        in () end