# HG changeset patch # User wenzelm # Date 1255816047 -7200 # Node ID fbc642835ecba753fd681e75b5141d2b7af7d93c # Parent 16ecd05c675c70a0e8b7c5f5464019a939f7dc36 made SML/NJ happy; diff -r 16ecd05c675c -r fbc642835ecb src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Oct 17 22:35:28 2009 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Oct 17 23:47:27 2009 +0200 @@ -307,8 +307,8 @@ (case hard_timeout of NONE => I | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs)) - val ({success, message, theorem_names, runtime=time_atp, ...}, time_isa) = - time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout + val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Wrapper.prover_result, + time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout in if success then (message, SH_OK (time_isa, time_atp, theorem_names)) else (message, SH_FAIL(time_isa, time_atp))