1.1 --- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Wed Jul 20 08:16:35 2011 +0200
     1.2 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Wed Jul 20 08:16:36 2011 +0200
     1.3 @@ -85,11 +85,11 @@
     1.4  
     1.5  ML {*
     1.6  val mtds = [
     1.7 -  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"random\") \"random\",
     1.8 -  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\",
     1.9 -  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\" #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\",
    1.10 -  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false) \"narrowing\",
    1.11 -  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false
    1.12 +  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\",
    1.13 +  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\",
    1.14 +  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\",
    1.15 +  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing\",
    1.16 +  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false
    1.17      #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"  
    1.18  (*  MutabelleExtra.nitpick_mtd *)
    1.19  ]

     2.1 --- a/src/Tools/quickcheck.ML	Wed Jul 20 08:16:35 2011 +0200
     2.2 +++ b/src/Tools/quickcheck.ML	Wed Jul 20 08:16:36 2011 +0200
     2.3 @@ -23,6 +23,7 @@
     2.4    val timeout : real Config.T
     2.5    val finite_types : bool Config.T
     2.6    val finite_type_size : int Config.T
     2.7 +  val set_active_testers: string list -> Context.generic -> Context.generic
     2.8    datatype expectation = No_Expectation | No_Counterexample | Counterexample;
     2.9    datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
    2.10    val test_params_of : Proof.context -> test_params