# HG changeset patch
# User bulwahn
# Date 1291986635 -3600
# Node ID 09037a02f5ec57815c19321123cfbbb473d74cd1
# Parent  a76ee71c3313b798b39d75fcae27933a3550b8b7
setting finite_type_size to 1 in mutabelle_extra

diff -r a76ee71c3313 -r 09037a02f5ec 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