--- 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