--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200
@@ -58,7 +58,7 @@
used_from : fact list,
preferred_methss : proof_method * proof_method list list,
run_time : Time.time,
- message : (string * stature) list * (proof_method * play_outcome) -> string}
+ message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
type prover = params -> prover_problem -> prover_result
@@ -149,7 +149,7 @@
used_from : fact list,
preferred_methss : proof_method * proof_method list list,
run_time : Time.time,
- message : (string * stature) list * (proof_method * play_outcome) -> string}
+ message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
type prover = params -> prover_problem -> prover_result