src/HOL/Mutabelle/mutabelle_extra.ML
changeset 41106 09037a02f5ec
parent 40974 29e5cae93584
child 41190 0bdc6fac5f48
--- 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