src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

   nontriv_success: int,
   proofs: int,
   time: int,
   timeout: int,
   lemmas: int * int * int,
-  posns: Position.T list
+  posns: (Position.T * bool) list
   }
 
 datatype min_data = MinData of {
   succs: int,
   ab_ratios: int

   log ("Average time for failed sledgehammer calls (ATP): " ^
     str3 (avg_time time_atp_fail (calls - success)))
   )
 
 
-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,
      metis_proofs, metis_time, metis_timeout, (lemmas, lems_sos, lems_max),
     metis_posns) =

     fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
       | with_time (true, t) = (change_data id (inc_metis_success m);
           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 =
       (with_time (Mirabelle.cpu_time apply_metis thms), true)
       handle TimeLimit.TimeOut => (change_data id (inc_metis_timeout m);