setting finite_type_size to 1 in mutabelle_extra
authorbulwahn
Fri, 10 Dec 2010 14:10:35 +0100
changeset 41106 09037a02f5ec
parent 41105 a76ee71c3313
child 41108 3f22550e442f
setting finite_type_size to 1 in mutabelle_extra
src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 10 11:42:05 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 10 14:10:35 2010 +0100
@@ -352,6 +352,7 @@
     can (TimeLimit.timeLimit (seconds 2.0)
       (Quickcheck.test_goal_terms
         ((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 [])) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
   end