# HG changeset patch
# User blanchet
# Date 1380006729 -7200
# Node ID 255a2929c137561fac5d7343fc021f2d9abf55ef
# Parent  0a62ad289c4d7ea8b58095090c32b9639db4f202
made SML/NJ happy

diff -r 0a62ad289c4d -r 255a2929c137 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Sep 23 16:56:17 2013 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Tue Sep 24 09:12:09 2013 +0200
@@ -100,7 +100,7 @@
                   " proof (of " ^ string_of_int (length facts) ^ "): ") "."
       |> Output.urgent_message
 
-    fun spying_str_of_res {outcome = NONE, used_facts, ...} =
+    fun spying_str_of_res ({outcome = NONE, used_facts, ...} : prover_result) =
         let val num_used_facts = length used_facts in
           "success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^
           plural_s num_used_facts