src/HOL/Mutabelle/mutabelle_extra.ML
changeset 41354 09037a02f5ec
parent 41220 29e5cae93584
child 41438 0bdc6fac5f48
     1.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 10 11:42:05 2010 +0100
     1.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 10 14:10:35 2010 +0100
     1.3 @@ -352,6 +352,7 @@
     1.4      can (TimeLimit.timeLimit (seconds 2.0)
     1.5        (Quickcheck.test_goal_terms
     1.6          ((Config.put Quickcheck.finite_types true #>
     1.7 +          Config.put Quickcheck.finite_type_size 1 #>
     1.8            Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
     1.9          false [])) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
    1.10    end