--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 23 22:37:16 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 23 23:10:13 2010 +0100
@@ -526,9 +526,12 @@
val (prover_name, _) = get_prover ctxt args
val minimize = AList.defined (op =) args minimizeK
val metis_ft = AList.defined (op =) args metis_ftK
- val trivial = TimeLimit.timeLimit try_outer_timeout
+ val trivial = false
+(* FIXME
+ TimeLimit.timeLimit try_outer_timeout
(Try.invoke_try (SOME try_inner_timeout)) pre
handle TimeLimit.TimeOut => false
+*)
fun apply_reconstructor m1 m2 =
if metis_ft
then