1.1 --- a/src/HOL/TPTP/mash_eval.ML	Tue Jul 31 12:38:01 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Tue Jul 31 14:42:03 2012 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4      val isar_ok = Unsynchronized.ref 0
     1.5      fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
     1.6      fun index_string (j, s) = s ^ "@" ^ string_of_int j
     1.7 -    fun str_of_res label facts {outcome, run_time, used_facts, ...} =
     1.8 +    fun str_of_res label facts ({outcome, run_time, used_facts, ...}: Sledgehammer_Provers.prover_result) =
     1.9        let val facts = facts |> map (fn ((name, _), _) => name ()) in
    1.10          "  " ^ label ^ ": " ^
    1.11          (if is_none outcome then