src/HOL/Mutabelle/mutabelle_extra.ML
changeset 45165 f4896c792316
parent 45159 3f1d1ce024cb
child 45397 20128348e9b9
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Oct 18 11:59:03 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Oct 18 15:27:17 2011 +0200
@@ -321,7 +321,8 @@
   in
     can (TimeLimit.timeLimit (seconds 2.0)
       (Quickcheck.test_terms
-        ((Config.put Quickcheck.finite_types true #>
+        ((Context.proof_map (Quickcheck.set_active_testers ["exhaustive"]) #>
+          Config.put Quickcheck.finite_types true #>
           Config.put Quickcheck.finite_type_size 1 #>
           Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
         (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy)