# HG changeset patch
# User blanchet
# Date 1291368519 -3600
# Node ID b9f56b4025d29aa3ce56ee8f673540326995f606
# Parent  061b8257ab9f61c94b790d1a611927e91238892c
compile

diff -r 061b8257ab9f -r b9f56b4025d2 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 03 09:55:45 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 03 10:28:39 2010 +0100
@@ -121,7 +121,7 @@
             (NONE, _) => (NoCex, ([], NONE))
           | (SOME _, _) => (GenuineCex, ([], NONE))) ()
   handle TimeLimit.TimeOut =>
-         (Timeout, ([("timelimit", Real.floor !Auto_Tools.time_limit)], NONE))
+         (Timeout, ([("timelimit", Real.floor (!Auto_Tools.time_limit))], NONE))
 
 fun quickcheck_mtd change_options quickcheck_generator =
   ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)