# HG changeset patch
# User blanchet
# Date 1280839782 -7200
# Node ID 7a88032f9265047149b5e555212f6fe6f979a968
# Parent  7207321df8afb87972e82b593287610a94204058
bump up the max cardinalities, to use up more of the time given to us by the user

diff -r 7207321df8af -r 7a88032f9265 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 03 14:49:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 03 14:49:42 2010 +0200
@@ -1374,7 +1374,8 @@
     case t |> strip_abs_body |> strip_comb of
       (Const x, ts as (_ :: _)) =>
       (case def_of_const thy table x of
-         SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso forall is_good_arg ts
+         SOME t' => fixpoint_kind_of_rhs t' <> NoFp andalso
+                    forall is_good_arg ts
        | NONE => false)
     | _ => false
   end
diff -r 7207321df8af -r 7a88032f9265 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Aug 03 14:49:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Aug 03 14:49:42 2010 +0200
@@ -34,10 +34,10 @@
 type raw_param = string * string list
 
 val default_default_params =
-  [("card", "1\<midarrow>8"),
-   ("iter", "0,1,2,4,8,12,16,24"),
-   ("bits", "1,2,3,4,6,8,10,12"),
-   ("bisim_depth", "7"),
+  [("card", "1\<midarrow>10"),
+   ("iter", "0,1,2,4,8,12,16,20,24,28"),
+   ("bits", "1,2,3,4,6,8,10,12,14,16"),
+   ("bisim_depth", "9"),
    ("box", "smart"),
    ("finitize", "smart"),
    ("mono", "smart"),
@@ -265,7 +265,7 @@
     val batch_size =
       case lookup_int_option "batch_size" of
         SOME n => Int.max (1, n)
-      | NONE => if debug then 1 else 64
+      | NONE => if debug then 1 else 50
     val expect = lookup_string "expect"
   in
     {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
diff -r 7207321df8af -r 7a88032f9265 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Aug 03 14:49:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Aug 03 14:49:42 2010 +0200
@@ -493,8 +493,8 @@
   | repair_cards_assigns_wrt_boxing_etc thy Ts ((NONE, ks) :: cards_assigns) =
     (NONE, ks) :: repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
 
-val max_scopes = 4096
-val distinct_threshold = 512
+val max_scopes = 5000
+val distinct_threshold = 1000
 
 fun all_scopes (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns
                iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs