diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -39,6 +39,7 @@
    ("bits", ["1,2,3,4,6,8,10,12"]),
    ("bisim_depth", ["7"]),
    ("box", ["smart"]),
+   ("finitize", ["smart"]),
    ("mono", ["smart"]),
    ("std", ["true"]),
    ("wf", ["smart"]),
@@ -78,6 +79,7 @@
 
 val negated_params =
   [("dont_box", "box"),
+   ("dont_finitize", "finitize"),
    ("non_mono", "mono"),
    ("non_std", "std"),
    ("non_wf", "wf"),
@@ -111,8 +113,8 @@
   AList.defined (op =) negated_params s orelse
   s = "max" orelse s = "eval" orelse s = "expect" orelse
   exists (fn p => String.isPrefix (p ^ " ") s)
-         ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "std",
-          "non_std", "wf", "non_wf", "format"]
+         ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
+          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
 
 (* string * 'a -> unit *)
 fun check_raw_param (s, _) =
@@ -297,14 +299,8 @@
     val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
     val bitss = lookup_int_seq "bits" 1
     val bisim_depths = lookup_int_seq "bisim_depth" ~1
-    val boxes =
-      lookup_bool_option_assigns read_type_polymorphic "box" @
-      map_filter (fn (SOME T, _) =>
-                     if is_fun_type T orelse is_pair_type T then
-                       SOME (SOME T, SOME true)
-                     else
-                       NONE
-                   | (NONE, _) => NONE) cards_assigns
+    val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
+    val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
     val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
     val stds = lookup_bool_assigns read_type_polymorphic "std"
     val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
@@ -349,8 +345,8 @@
   in
     {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
      iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
-     boxes = boxes, monos = monos, stds = stds, wfs = wfs,
-     sat_solver = sat_solver, blocking = blocking, falsify = falsify,
+     boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,
+     wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
      debug = debug, verbose = verbose, overlord = overlord,
      user_axioms = user_axioms, assms = assms,
      merge_type_vars = merge_type_vars, binary_ints = binary_ints,