# HG changeset patch
# User wenzelm
# Date 1343738523 -7200
# Node ID d5c9917ff5b6ac12d9bee90c25cc5870e2bc6c49
# Parent  6004f45756456952f73567fc77bfa4575052b4e9
made SML/NJ happy;

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