# HG changeset patch
# User blanchet
# Date 1284383470 -7200
# Node ID d2b981a0429ae3508eec92a7b2e795c95e0f1dcc
# Parent  3998dc0bf82be36874dab201685f029ba6a97b14
indicate triviality in the list of proved things

diff -r 3998dc0bf82b -r d2b981a0429a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 13 15:01:31 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 13 15:11:10 2010 +0200
@@ -41,7 +41,7 @@
   time: int,
   timeout: int,
   lemmas: int * int * int,
-  posns: Position.T list
+  posns: (Position.T * bool) list
   }
 
 datatype min_data = MinData of {
@@ -234,9 +234,12 @@
   )
 
 
-fun str_of_pos pos =
+fun str_of_pos (pos, triv) =
   let val str0 = string_of_int o the_default 0
-  in str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) end
+  in
+    str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) ^
+    (if triv then "[T]" else "")
+  end
 
 fun log_me_data log tag sh_calls (metis_calls, metis_success,
      metis_nontriv_calls, metis_nontriv_success,
@@ -470,7 +473,7 @@
           if trivial then () else change_data id (inc_metis_nontriv_success m);
           change_data id (inc_metis_lemmas m (length named_thms));
           change_data id (inc_metis_time m t);
-          change_data id (inc_metis_posns m pos);
+          change_data id (inc_metis_posns m (pos, trivial));
           if name = "proof" then change_data id (inc_metis_proofs m) else ();
           "succeeded (" ^ string_of_int t ^ ")")
     fun timed_metis thms =