1.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Dec 14 16:48:49 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Dec 17 15:22:11 2009 +0100
     1.3 @@ -37,6 +37,7 @@
     1.4  val default_default_params =
     1.5    [("card", ["1\<midarrow>8"]),
     1.6     ("iter", ["0,1,2,4,8,12,16,24"]),
     1.7 +   ("bits", ["1,2,3,4,6,8,10,12"]),
     1.8     ("bisim_depth", ["7"]),
     1.9     ("box", ["smart"]),
    1.10     ("mono", ["smart"]),
    1.11 @@ -48,6 +49,7 @@
    1.12     ("user_axioms", ["smart"]),
    1.13     ("assms", ["true"]),
    1.14     ("merge_type_vars", ["false"]),
    1.15 +   ("binary_ints", ["smart"]),
    1.16     ("destroy_constrs", ["true"]),
    1.17     ("specialize", ["true"]),
    1.18     ("skolemize", ["true"]),
    1.19 @@ -83,6 +85,7 @@
    1.20     ("no_user_axioms", "user_axioms"),
    1.21     ("no_assms", "assms"),
    1.22     ("dont_merge_type_vars", "merge_type_vars"),
    1.23 +   ("unary_ints", "binary_ints"),
    1.24     ("dont_destroy_constrs", "destroy_constrs"),
    1.25     ("dont_specialize", "specialize"),
    1.26     ("dont_skolemize", "skolemize"),
    1.27 @@ -283,6 +286,7 @@
    1.28      val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
    1.29      val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
    1.30      val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
    1.31 +    val bitss = lookup_int_seq "bits" 1
    1.32      val bisim_depths = lookup_int_seq "bisim_depth" ~1
    1.33      val boxes =
    1.34        lookup_bool_option_assigns read_type_polymorphic "box" @
    1.35 @@ -303,6 +307,7 @@
    1.36      val user_axioms = lookup_bool_option "user_axioms"
    1.37      val assms = lookup_bool "assms"
    1.38      val merge_type_vars = lookup_bool "merge_type_vars"
    1.39 +    val binary_ints = lookup_bool_option "binary_ints"
    1.40      val destroy_constrs = lookup_bool "destroy_constrs"
    1.41      val specialize = lookup_bool "specialize"
    1.42      val skolemize = lookup_bool "skolemize"
    1.43 @@ -333,15 +338,16 @@
    1.44      val expect = lookup_string "expect"
    1.45    in
    1.46      {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
    1.47 -     iters_assigns = iters_assigns, bisim_depths = bisim_depths, boxes = boxes,
    1.48 -     monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
    1.49 -     falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,
    1.50 -     user_axioms = user_axioms, assms = assms,
    1.51 -     merge_type_vars = merge_type_vars, destroy_constrs = destroy_constrs,
    1.52 -     specialize = specialize, skolemize = skolemize,
    1.53 -     star_linear_preds = star_linear_preds, uncurry = uncurry,
    1.54 -     fast_descrs = fast_descrs, peephole_optim = peephole_optim,
    1.55 -     timeout = timeout, tac_timeout = tac_timeout, sym_break = sym_break,
    1.56 +     iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
    1.57 +     boxes = boxes, monos = monos, wfs = wfs, sat_solver = sat_solver,
    1.58 +     blocking = blocking, falsify = falsify, debug = debug, verbose = verbose,
    1.59 +     overlord = overlord, user_axioms = user_axioms, assms = assms,
    1.60 +     merge_type_vars = merge_type_vars, binary_ints = binary_ints,
    1.61 +     destroy_constrs = destroy_constrs, specialize = specialize,
    1.62 +     skolemize = skolemize, star_linear_preds = star_linear_preds,
    1.63 +     uncurry = uncurry, fast_descrs = fast_descrs,
    1.64 +     peephole_optim = peephole_optim, timeout = timeout,
    1.65 +     tac_timeout = tac_timeout, sym_break = sym_break,
    1.66       sharing_depth = sharing_depth, flatten_props = flatten_props,
    1.67       max_threads = max_threads, show_skolems = show_skolems,
    1.68       show_datatypes = show_datatypes, show_consts = show_consts,
    1.69 @@ -379,8 +385,6 @@
    1.70           error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
    1.71         | BAD (loc, details) =>
    1.72           error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
    1.73 -       | LIMIT (_, details) =>
    1.74 -         (warning ("Limit reached: " ^ details ^ "."); x)
    1.75         | NOT_SUPPORTED details =>
    1.76           (warning ("Unsupported case: " ^ details ^ "."); x)
    1.77         | NUT (loc, us) =>
    1.78 @@ -394,6 +398,10 @@
    1.79           error ("Invalid term" ^ plural_s_for_list ts ^
    1.80                  " (" ^ quote loc ^ "): " ^
    1.81                  commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
    1.82 +       | TOO_LARGE (_, details) =>
    1.83 +         (warning ("Limit reached: " ^ details ^ "."); x)
    1.84 +       | TOO_SMALL (_, details) =>
    1.85 +         (warning ("Limit reached: " ^ details ^ "."); x)
    1.86         | TYPE (loc, Ts, ts) =>
    1.87           error ("Invalid type" ^ plural_s_for_list Ts ^
    1.88                  (if null ts then