diff -r c2e1503fad8f -r 3c029ef9e0f2 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 18 17:27:28 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 18 22:55:28 2011 +0100
@@ -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