# HG changeset patch
# User blanchet
# Date 1284382891 -7200
# Node ID 3998dc0bf82be36874dab201685f029ba6a97b14
# Parent  9608a5bd5d207c1fb046aa05b3708e3f07de75f1
indicate which goals are trivial

diff -r 9608a5bd5d20 -r 3998dc0bf82b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 13 14:30:21 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 13 15:01:31 2010 +0200
@@ -388,6 +388,7 @@
 
 fun run_sledgehammer trivial args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
   let
+    val triv_str = if trivial then "[T] " else ""
     val _ = change_data id inc_sh_calls
     val _ = if trivial then () else change_data id inc_sh_nontriv_calls
     val (prover_name, prover) = get_atp (Proof.theory_of st) args
@@ -411,14 +412,14 @@
           change_data id (inc_sh_time_isa time_isa);
           change_data id (inc_sh_time_atp time_atp);
           named_thms := SOME (map_filter get_thms names);
-          log (sh_tag id ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
+          log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
             string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
         end
     | SH_FAIL (time_isa, time_atp) =>
         let
           val _ = change_data id (inc_sh_time_isa time_isa)
           val _ = change_data id (inc_sh_time_atp_fail time_atp)
-        in log (sh_tag id ^ "failed: " ^ msg) end
+        in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end
     | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
   end