--- 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
+
]
*}
--- 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 #>