# HG changeset patch
# User blanchet
# Date 1348758054 -7200
# Node ID 29be73b789f920ab4f6f9ba2d3e644d4307a59ff
# Parent  7ec6471f8388942b0bb8daa11a18575417c26b4e
lower the defaults for the number of bits, based on an example by Lukas Bulwahn

diff -r 7ec6471f8388 -r 29be73b789f9 src/Doc/Nitpick/document/root.tex
--- a/src/Doc/Nitpick/document/root.tex	Thu Sep 27 17:00:54 2012 +0200
+++ b/src/Doc/Nitpick/document/root.tex	Thu Sep 27 17:00:54 2012 +0200
@@ -2032,7 +2032,7 @@
 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
 \textit{show\_datatypes} (\S\ref{output-format}).}
 
-\opdefault{bits}{int\_seq}{\upshape 1,2,3,4,6,8,10,12,14,16}
+\opdefault{bits}{int\_seq}{\upshape 1--10}
 Specifies the number of bits to use to represent natural numbers and integers in
 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
 
diff -r 7ec6471f8388 -r 29be73b789f9 src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Sep 27 17:00:54 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Sep 27 17:00:54 2012 +0200
@@ -20,7 +20,7 @@
       (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
     (term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
      thm list list) * local_theory
-  val parse_wrap_options: bool parser
+  val parse_wrap_options: (bool * bool) parser
   val parse_bound_term: (binding * string) parser
 end;
 
diff -r 7ec6471f8388 -r 29be73b789f9 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Sep 27 17:00:54 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Sep 27 17:00:54 2012 +0200
@@ -44,7 +44,7 @@
 val default_default_params =
   [("card", "1\<emdash>10"),
    ("iter", "0,1,2,4,8,12,16,20,24,28"),
-   ("bits", "1,2,3,4,6,8,10,12,14,16"),
+   ("bits", "1\<emdash>10"),
    ("bisim_depth", "9"),
    ("box", "smart"),
    ("finitize", "smart"),