# HG changeset patch
# User bulwahn
# Date 1328956581 -3600
# Node ID e4f1cda51df6d043550964cd3ddfa9ce35a23512
# Parent  4989249a4b81747ce049ea547f600f6dc536fd1b
increase timeout to 30 seconds; changing mutabelle script

diff -r 4989249a4b81 -r e4f1cda51df6 src/HOL/Mutabelle/lib/Tools/mutabelle
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Fri Feb 10 17:10:49 2012 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Sat Feb 11 11:36:21 2012 +0100
@@ -101,10 +101,10 @@
   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_no_finite_types\",
   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false
     #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
-(*
-, MutabelleExtra.refute_mtd,
-  MutabelleExtra.nitpick_mtd
-*)
+
+(*, MutabelleExtra.refute_mtd, *)
+  , MutabelleExtra.nitpick_mtd
+
 ]
 *}
 
diff -r 4989249a4b81 -r e4f1cda51df6 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Feb 10 17:10:49 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Feb 11 11:36:21 2012 +0100
@@ -117,7 +117,7 @@
 (** quickcheck **)
 
 fun invoke_quickcheck change_options quickcheck_generator thy t =
-  TimeLimit.timeLimit (seconds (!Try.auto_time_limit))
+  TimeLimit.timeLimit (seconds 30.0)
       (fn _ =>
           let
             val ctxt' = change_options (Proof_Context.init_global thy)
@@ -324,7 +324,7 @@
   let
     val ctxt = Proof_Context.init_global thy
   in
-    can (TimeLimit.timeLimit (seconds 2.0)
+    can (TimeLimit.timeLimit (seconds 30.0)
       (Quickcheck.test_terms
         ((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #>
           Config.put Quickcheck.finite_types true #>