--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Wed Jul 20 08:16:35 2011 +0200
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Wed Jul 20 08:16:36 2011 +0200
@@ -85,11 +85,11 @@
ML {*
val mtds = [
- MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"random\") \"random\",
- MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\",
- MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\" #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\",
- MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false) \"narrowing\",
- MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false
+ MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\",
+ MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\",
+ MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\",
+ MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing\",
+ 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.nitpick_mtd *)
]