author | bulwahn |
Mon, 06 Dec 2010 10:52:44 +0100 | |
changeset 40972 | ce78ef6a909b |
parent 40971 | 6604115019bf |
child 40973 | 890fefa597af |
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Dec 06 10:52:43 2010 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Dec 06 10:52:44 2010 +0100 @@ -148,7 +148,7 @@ let val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) in - case Try.invoke_try NONE state of + case Try.invoke_try (SOME (seconds 5.0)) state of true => (Solved, ([], NONE)) | false => (Unsolved, ([], NONE)) end