changeset 41999 | 3c029ef9e0f2 |
parent 41755 | 404d94506599 |
child 42012 | 2c3fe3cbebae |
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 18 17:27:28 2011 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 18 22:55:28 2011 +0100 @@ -150,7 +150,7 @@ let val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) in - case Try.invoke_try (SOME (seconds 5.0)) state of + case Try.invoke_try (SOME (seconds 5.0)) ([], [], []) state of true => (Solved, ([], NONE)) | false => (Unsolved, ([], NONE)) end