--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 31 09:43:36 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Mar 31 11:16:51 2011 +0200
@@ -558,7 +558,7 @@
Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
- val trivial = Try.invoke_try (SOME try_timeout) ([], [], []) pre
+ val trivial = Try.invoke_try (SOME try_timeout) ([], [], [], []) pre
handle TimeLimit.TimeOut => false
fun apply_reconstructor m1 m2 =
if metis_ft