# HG changeset patch
# User blanchet
# Date 1266437620 -3600
# Node ID a815c3f4eef2274249c2dad29af4ce987b0c8f89
# Parent  69fa4c39dab28528c319c988928aef012aca7ddb# Parent  3b9762ad372d5ac906c7e50106e231f3a459a17b
merged

diff -r 3b9762ad372d -r a815c3f4eef2 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Wed Feb 17 11:31:15 2010 -0800
+++ b/doc-src/Nitpick/nitpick.tex	Wed Feb 17 21:13:40 2010 +0100
@@ -472,7 +472,9 @@
 \prew
 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
 \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
-\slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
+\slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported
+fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
+Nitpick found a potential counterexample: \\[2\smallskipamount]
 \hbox{}\qquad Free variable: \nopagebreak \\
 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
 Confirmation by ``\textit{auto}'': The above counterexample is genuine.
@@ -1331,7 +1333,7 @@
 and this time \textit{arith} can finish off the subgoals.
 
 A similar technique can be employed for structural induction. The
-following mini-formalization of full binary trees will serve as illustration:
+following mini formalization of full binary trees will serve as illustration:
 
 \prew
 \textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount]
@@ -1350,8 +1352,7 @@
 obtained by swapping $a$ and $b$:
 
 \prew
-\textbf{lemma} $``\lbrakk a \in \textit{labels}~t;\, b \in \textit{labels}~t;\, a \not= b\rbrakk {}$ \\
-\phantom{\textbf{lemma} ``}$\,{\Longrightarrow}{\;\,} \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
+\textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
 \postw
 
 Nitpick can't find any counterexample, so we proceed with induction
@@ -1369,48 +1370,47 @@
 
 \prew
 \slshape
-Hint: To check that the induction hypothesis is general enough, try the following command:
-\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
+Hint: To check that the induction hypothesis is general enough, try this command:
+\textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}].
 \postw
 
 If we follow the hint, we get a ``nonstandard'' counterexample for the step:
 
 \prew
-\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
+\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
 \hbox{}\qquad Free variables: \nopagebreak \\
 \hbox{}\qquad\qquad $a = a_1$ \\
 \hbox{}\qquad\qquad $b = a_2$ \\
 \hbox{}\qquad\qquad $t = \xi_1$ \\
 \hbox{}\qquad\qquad $u = \xi_2$ \\
+\hbox{}\qquad Datatype: \nopagebreak \\
+\hbox{}\qquad\qquad $\alpha~\textit{btree} = \{\xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \textit{Branch}~\xi_1~\xi_2\}$ \\
 \hbox{}\qquad {\slshape Constants:} \nopagebreak \\
 \hbox{}\qquad\qquad $\textit{labels} = \undef
     (\!\begin{aligned}[t]%
-    & \xi_1 := \{a_1, a_4, a_3^\Q\},\> \xi_2 := \{a_2, a_3^\Q\}, \\[-2pt] %% TYPESETTING
-    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_4, a_3^\Q\}, \\[-2pt]
-    & \textit{Branch}~\xi_2~\xi_2 := \{a_2, a_3^\Q\})\end{aligned}$ \\
+    & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
+    & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
 \hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
     (\!\begin{aligned}[t]%
     & \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
-    & \textit{Branch}~\xi_1~\xi_2 := \textit{Branch}~\xi_2~\xi_2, \\[-2pt]
-    & \textit{Branch}~\xi_2~\xi_2 := \textit{Branch}~\xi_2~\xi_2)\end{aligned}$ \\[2\smallskipamount]
+    & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
 The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
 even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
 \postw
 
 Reading the Nitpick manual is a most excellent idea.
-But what's going on? The \textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$''
-option told the tool to look for nonstandard models of binary trees, which
-means that new ``nonstandard'' trees $\xi_1, \xi_2, \ldots$, are now allowed in
-addition to the standard trees generated by the \textit{Leaf} and
-\textit{Branch} constructors.%
+But what's going on? The \textit{non\_std} option told the tool to look for
+nonstandard models of binary trees, which means that new ``nonstandard'' trees
+$\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees
+generated by the \textit{Leaf} and \textit{Branch} constructors.%
 \footnote{Notice the similarity between allowing nonstandard trees here and
 allowing unreachable states in the preceding example (by removing the ``$n \in
 \textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
 set of objects over which the induction is performed while doing the step
 in order to test the induction hypothesis's strength.}
-The new trees are so nonstandard that we know nothing about them, except what
-the induction hypothesis states and what can be proved about all trees without
-relying on induction or case distinction. The key observation is,
+Unlike standard trees, these new trees contain cycles. We will see later that
+every property of acyclic trees that can be proved without using induction also
+holds for cyclic trees. Hence,
 %
 \begin{quote}
 \textsl{If the induction
@@ -1418,9 +1418,9 @@
 objects, and Nitpick won't find any nonstandard counterexample.}
 \end{quote}
 %
-But here, Nitpick did find some nonstandard trees $t = \xi_1$
-and $u = \xi_2$ such that $a \in \textit{labels}~t$, $b \notin
-\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
+But here the tool find some nonstandard trees $t = \xi_1$
+and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
+\textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
 Because neither tree contains both $a$ and $b$, the induction hypothesis tells
 us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
 and as a result we know nothing about the labels of the tree
@@ -2080,9 +2080,10 @@
 {\small See also \textit{mono} (\S\ref{scope-of-search}).}
 
 \opargbool{std}{type}{non\_std}
-Specifies whether the given type should be given standard models.
-Nonstandard models are unsound but can help debug inductive arguments,
-as explained in \S\ref{inductive-properties}.
+Specifies whether the given (recursive) datatype should be given standard
+models. Nonstandard models are unsound but can help debug structural induction
+proofs, as explained in \S\ref{inductive-properties}.
+%This option is not supported for the type \textit{nat}.
 
 \optrue{std}{non\_std}
 Specifies the default standardness to use. This can be overridden on a per-type
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Nitpick.thy	Wed Feb 17 21:13:40 2010 +0100
@@ -37,7 +37,6 @@
            and bisim_iterator_max :: bisim_iterator
            and Quot :: "'a \<Rightarrow> 'b"
            and quot_normal :: "'a \<Rightarrow> 'a"
-           and NonStd :: "'a \<Rightarrow> 'b"
            and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
 
 datatype ('a, 'b) pair_box = PairBox 'a 'b
@@ -45,7 +44,6 @@
 
 typedecl unsigned_bit
 typedecl signed_bit
-typedecl \<xi>
 
 datatype 'a word = Word "('a set)"
 
@@ -254,12 +252,12 @@
 setup {* Nitpick_Isar.setup *}
 
 hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
-    bisim_iterator_max Quot quot_normal NonStd Tha PairBox FunBox Word refl' wf'
+    bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf'
     wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
     int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
     plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
     of_frac
-hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit \<xi> word
+hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
 hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
     wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
     The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Feb 17 21:13:40 2010 +0100
@@ -259,14 +259,14 @@
  (if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
 "swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
 
-lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t"
+lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
 nitpick
 proof (induct t)
   case Leaf thus ?case by simp
 next
   case (Branch t u) thus ?case
   nitpick
-  nitpick [non_std "'a bin_tree", show_consts]
+  nitpick [non_std, show_all]
 oops
 
 lemma "labels (swap t a b) =
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Feb 17 21:13:40 2010 +0100
@@ -29,7 +29,7 @@
    special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
    wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
 (* term -> bool *)
-val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt @{typ 'a}
+val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a}
                                               Nitpick_Mono.Plus [] []
 fun is_const t =
   let val T = fastype_of t in
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -167,6 +167,7 @@
 
   val max_arity : int -> int
   val arity_of_rel_expr : rel_expr -> int
+  val is_problem_trivially_false : problem -> bool
   val problems_equivalent : problem -> problem -> bool
   val solve_any_problem :
     bool -> Time.time option -> int -> int -> problem list -> outcome
@@ -491,6 +492,10 @@
   | arity_of_decl (DeclSome ((n, _), _)) = n
   | arity_of_decl (DeclSet ((n, _), _)) = n
 
+(* problem -> bool *)
+fun is_problem_trivially_false ({formula = False, ...} : problem) = true
+  | is_problem_trivially_false _ = false
+
 (* string -> bool *)
 val is_relevant_setting = not o member (op =) ["solver", "delay"]
 
@@ -1014,8 +1019,8 @@
     val indexed_problems = if j >= 0 then
                              [(j, nth problems j)]
                            else
-                             filter (not_equal False o #formula o snd)
-                                    (0 upto length problems - 1 ~~ problems)
+                             filter_out (is_problem_trivially_false o snd)
+                                        (0 upto length problems - 1 ~~ problems)
     val triv_js = filter_out (AList.defined (op =) indexed_problems)
                              (0 upto length problems - 1)
     (* int -> int *)
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -9,7 +9,7 @@
 sig
   val configured_sat_solvers : bool -> string list
   val smart_sat_solver_name : bool -> string
-  val sat_solver_spec : bool -> string -> string * string list
+  val sat_solver_spec : string -> string * string list
 end;
 
 structure Kodkod_SAT : KODKOD_SAT =
@@ -51,15 +51,15 @@
    ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
                             "s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
 
-(* bool -> string -> sink -> string -> string -> string list -> string list
+(* string -> sink -> string -> string -> string list -> string list
    -> (string * (unit -> string list)) option *)
-fun dynamic_entry_for_external overlord name dev home exec args markers =
+fun dynamic_entry_for_external name dev home exec args markers =
   case getenv home of
     "" => NONE
   | dir =>
     SOME (name, fn () =>
                    let
-                     val serial_str = if overlord then "" else serial_string ()
+                     val serial_str = serial_string ()
                      val base = name ^ serial_str
                      val out_file = base ^ ".out"
                      val dir_sep =
@@ -76,9 +76,9 @@
                    end)
 (* bool -> bool -> string * sat_solver_info
    -> (string * (unit -> string list)) option *)
-fun dynamic_entry_for_info _ incremental (name, Internal (Java, mode, ss)) =
+fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
     if incremental andalso mode = Batch then NONE else SOME (name, K ss)
-  | dynamic_entry_for_info _ incremental (name, Internal (JNI, mode, ss)) =
+  | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =
     if incremental andalso mode = Batch then
       NONE
     else
@@ -92,26 +92,25 @@
         else
           NONE
       end
-  | dynamic_entry_for_info overlord false
-    (name, External (dev, home, exec, args)) =
-    dynamic_entry_for_external overlord name dev home exec args []
-  | dynamic_entry_for_info overlord false
+  | dynamic_entry_for_info false (name, External (dev, home, exec, args)) =
+    dynamic_entry_for_external name dev home exec args []
+  | dynamic_entry_for_info false
         (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
-    dynamic_entry_for_external overlord name dev home exec args [m1, m2, m3]
-  | dynamic_entry_for_info _ true _ = NONE
-(* bool -> bool -> (string * (unit -> string list)) list *)
-fun dynamic_list overlord incremental =
-  map_filter (dynamic_entry_for_info overlord incremental) static_list
+    dynamic_entry_for_external name dev home exec args [m1, m2, m3]
+  | dynamic_entry_for_info true _ = NONE
+(* bool -> (string * (unit -> string list)) list *)
+fun dynamic_list incremental =
+  map_filter (dynamic_entry_for_info incremental) static_list
 
 (* bool -> string list *)
-val configured_sat_solvers = map fst o dynamic_list false
+val configured_sat_solvers = map fst o dynamic_list
 (* bool -> string *)
-val smart_sat_solver_name = fst o hd o dynamic_list false
+val smart_sat_solver_name = fst o hd o dynamic_list
 
-(* bool -> string -> string * string list *)
-fun sat_solver_spec overlord name =
+(* string -> string * string list *)
+fun sat_solver_spec name =
   let
-    val dyn_list = dynamic_list overlord false
+    val dyn_list = dynamic_list false
     (* (string * 'a) list -> string *)
     fun enum_solvers solvers =
       commas (distinct (op =) (map (quote o fst) solvers))
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -84,7 +84,7 @@
 fun atom_from_formula f = RelIf (f, true_atom, false_atom)
 
 (* Proof.context -> (typ -> int) -> styp list -> term -> formula *)
-fun kodkod_formula_for_term ctxt card frees =
+fun kodkod_formula_from_term ctxt card frees =
   let
     (* typ -> rel_expr -> rel_expr *)
     fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r =
@@ -145,7 +145,7 @@
        | Term.Var _ => raise SAME ()
        | Bound _ => raise SAME ()
        | Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
-       | _ => raise TERM ("Minipick.kodkod_formula_for_term.to_F", [t]))
+       | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
       handle SAME () => formula_from_atom (to_R_rep Ts t)
     (* typ list -> term -> rel_expr *)
     and to_S_rep Ts t =
@@ -306,7 +306,7 @@
     val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
     val declarative_axioms =
       map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
-    val formula = kodkod_formula_for_term ctxt card frees neg_t
+    val formula = kodkod_formula_from_term ctxt card frees neg_t
                   |> fold_rev (curry And) declarative_axioms
     val univ_card = univ_card 0 0 0 bounds formula
     val problem =
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -130,7 +130,7 @@
   sel_names: nut list,
   nonsel_names: nut list,
   rel_table: nut NameTable.table,
-  liberal: bool,
+  unsound: bool,
   scope: scope,
   core: KK.formula,
   defs: KK.formula list}
@@ -157,15 +157,15 @@
       (Path.variable "ISABELLE_HOME_USER" ::
        map Path.basic ["etc", "components"]))) ^ "\"."
 
-val max_liberal_delay_ms = 200
-val max_liberal_delay_percent = 2
+val max_unsound_delay_ms = 200
+val max_unsound_delay_percent = 2
 
 (* Time.time option -> int *)
-fun liberal_delay_for_timeout NONE = max_liberal_delay_ms
-  | liberal_delay_for_timeout (SOME timeout) =
-    Int.max (0, Int.min (max_liberal_delay_ms,
+fun unsound_delay_for_timeout NONE = max_unsound_delay_ms
+  | unsound_delay_for_timeout (SOME timeout) =
+    Int.max (0, Int.min (max_unsound_delay_ms,
                          Time.toMilliseconds timeout
-                         * max_liberal_delay_percent div 100))
+                         * max_unsound_delay_percent div 100))
 
 (* Time.time option -> bool *)
 fun passed_deadline NONE = false
@@ -247,7 +247,7 @@
                 (if i <> 1 orelse n <> 1 then
                    "subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
                  else
-                   "goal")) [orig_t]))
+                   "goal")) [Logic.list_implies (orig_assm_ts, orig_t)]))
     val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
                 else orig_t
     val assms_t = if assms orelse auto then
@@ -293,7 +293,7 @@
     val _ = null (Term.add_tvars assms_t []) orelse
             raise NOT_SUPPORTED "schematic type variables"
     val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
-         core_t) = preprocess_term hol_ctxt assms_t
+         core_t, binarize) = preprocess_term hol_ctxt assms_t
     val got_all_user_axioms =
       got_all_mono_user_axioms andalso no_poly_user_axioms
 
@@ -345,12 +345,13 @@
       case triple_lookup (type_match thy) monos T of
         SOME (SOME b) => b
       | _ => is_type_always_monotonic T orelse
-             formulas_monotonic hol_ctxt T Plus def_ts nondef_ts core_t
+             formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t
     fun is_deep_datatype T =
       is_datatype thy T andalso
-      (is_word_type T orelse
+      (not standard orelse is_word_type T orelse
        exists (curry (op =) T o domain_type o type_of) sel_names)
-    val all_Ts = ground_types_in_terms hol_ctxt (core_t :: def_ts @ nondef_ts)
+    val all_Ts = ground_types_in_terms hol_ctxt binarize
+                                       (core_t :: def_ts @ nondef_ts)
                  |> sort TermOrd.typ_ord
     val _ = if verbose andalso binary_ints = SOME true andalso
                exists (member (op =) [nat_T, int_T]) all_Ts then
@@ -382,29 +383,22 @@
       else
         ()
     val deep_dataTs = filter is_deep_datatype all_Ts
-    (* FIXME: Implement proper detection of induction datatypes. *)
+    (* This detection code is an ugly hack. Fortunately, it is used only to
+       provide a hint to the user. *)
     (* string * (Rule_Cases.T * bool) -> bool *)
-    fun is_inductive_case (_, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
-      false
-(*
-      not (null fixes) andalso exists (String.isSuffix ".hyps" o fst) assumes
-*)
-    (* unit -> typ list *)
-    val induct_dataTs =
-      if exists is_inductive_case (ProofContext.cases_of ctxt) then
-        filter (is_datatype thy) all_Ts
-      else
-        []
-    val _ = if standard andalso not (null induct_dataTs) then
+    fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
+      not (null fixes) andalso
+      exists (String.isSuffix ".hyps" o fst) assumes andalso
+      exists (exists (curry (op =) name o shortest_name o fst)
+              o datatype_constrs hol_ctxt) deep_dataTs
+    val likely_in_struct_induct_step =
+      exists is_struct_induct_step (ProofContext.cases_of ctxt)
+    val _ = if standard andalso likely_in_struct_induct_step then
               pprint_m (fn () => Pretty.blk (0,
                   pstrs "Hint: To check that the induction hypothesis is \
-                        \general enough, try the following command: " @
+                        \general enough, try this command: " @
                   [Pretty.mark Markup.sendback (Pretty.blk (0,
-                       pstrs ("nitpick [" ^
-                              commas (map (prefix "non_std " o maybe_quote
-                                           o unyxml o string_for_type ctxt)
-                                          induct_dataTs) ^
-                              ", show_consts]")))] @ pstrs "."))
+                       pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
             else
               ()
 (*
@@ -441,7 +435,7 @@
     val too_big_scopes = Unsynchronized.ref []
 
     (* bool -> scope -> rich_problem option *)
-    fun problem_for_scope liberal
+    fun problem_for_scope unsound
             (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
       let
         val _ = not (exists (fn other => scope_less_eq other scope)
@@ -476,10 +470,10 @@
                          (univ_card nat_card int_card main_j0 [] KK.True)
         val _ = check_arity min_univ_card min_highest_arity
 
-        val core_u = choose_reps_in_nut scope liberal rep_table false core_u
-        val def_us = map (choose_reps_in_nut scope liberal rep_table true)
+        val core_u = choose_reps_in_nut scope unsound rep_table false core_u
+        val def_us = map (choose_reps_in_nut scope unsound rep_table true)
                          def_us
-        val nondef_us = map (choose_reps_in_nut scope liberal rep_table false)
+        val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
                             nondef_us
 (*
         val _ = List.app (priority o string_for_nut ctxt)
@@ -495,21 +489,19 @@
         val core_u = rename_vars_in_nut pool rel_table core_u
         val def_us = map (rename_vars_in_nut pool rel_table) def_us
         val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
-        (* nut -> KK.formula *)
-        val to_f = kodkod_formula_from_nut bits ofs liberal kk
-        val core_f = to_f core_u
-        val def_fs = map to_f def_us
-        val nondef_fs = map to_f nondef_us
+        val core_f = kodkod_formula_from_nut bits ofs kk core_u
+        val def_fs = map (kodkod_formula_from_nut bits ofs kk) def_us
+        val nondef_fs = map (kodkod_formula_from_nut bits ofs kk) nondef_us
         val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
-        val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
+        val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
                       PrintMode.setmp [] multiline_string_for_scope scope
         val kodkod_sat_solver =
-          Kodkod_SAT.sat_solver_spec overlord effective_sat_solver |> snd
+          Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd
         val bit_width = if bits = 0 then 16 else bits + 1
-        val delay = if liberal then
+        val delay = if unsound then
                       Option.map (fn time => Time.- (time, Time.now ()))
                                  deadline
-                      |> liberal_delay_for_timeout
+                      |> unsound_delay_for_timeout
                     else
                       0
         val settings = [("solver", commas (map quote kodkod_sat_solver)),
@@ -523,8 +515,9 @@
         val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
         val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
         val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
-        val dtype_axioms = declarative_axioms_for_datatypes hol_ctxt bits ofs kk
-                                                            rel_table datatypes
+        val dtype_axioms =
+          declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk
+                                           rel_table datatypes
         val declarative_axioms = plain_axioms @ dtype_axioms
         val univ_card = univ_card nat_card int_card main_j0
                                   (plain_bounds @ sel_bounds) formula
@@ -547,29 +540,30 @@
                expr_assigns = [], formula = formula},
               {free_names = free_names, sel_names = sel_names,
                nonsel_names = nonsel_names, rel_table = rel_table,
-               liberal = liberal, scope = scope, core = core_f,
+               unsound = unsound, scope = scope, core = core_f,
                defs = nondef_fs @ def_fs @ declarative_axioms})
       end
       handle TOO_LARGE (loc, msg) =>
              if loc = "Nitpick_Kodkod.check_arity" andalso
                 not (Typtab.is_empty ofs) then
-               problem_for_scope liberal
-                   {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
-                    bits = bits, bisim_depth = bisim_depth,
-                    datatypes = datatypes, ofs = Typtab.empty}
+               problem_for_scope unsound
+                   {hol_ctxt = hol_ctxt, binarize = binarize,
+                    card_assigns = card_assigns, bits = bits,
+                    bisim_depth = bisim_depth, datatypes = datatypes,
+                    ofs = Typtab.empty}
              else if loc = "Nitpick.pick_them_nits_in_term.\
                            \problem_for_scope" then
                NONE
              else
                (Unsynchronized.change too_big_scopes (cons scope);
                 print_v (fn () => ("Limit reached: " ^ msg ^
-                                   ". Skipping " ^ (if liberal then "potential"
+                                   ". Skipping " ^ (if unsound then "potential"
                                                     else "genuine") ^
                                    " component of scope."));
                 NONE)
            | TOO_SMALL (loc, msg) =>
              (print_v (fn () => ("Limit reached: " ^ msg ^
-                                 ". Skipping " ^ (if liberal then "potential"
+                                 ". Skipping " ^ (if unsound then "potential"
                                                   else "genuine") ^
                                  " component of scope."));
               NONE)
@@ -584,7 +578,7 @@
 
     val scopes = Unsynchronized.ref []
     val generated_scopes = Unsynchronized.ref []
-    val generated_problems = Unsynchronized.ref []
+    val generated_problems = Unsynchronized.ref ([] : rich_problem list)
     val checked_problems = Unsynchronized.ref (SOME [])
     val met_potential = Unsynchronized.ref 0
 
@@ -635,7 +629,7 @@
               | NONE => print "No confirmation by \"auto\".")
            else
              ();
-           if not standard andalso not (null induct_dataTs) then
+           if not standard andalso likely_in_struct_induct_step then
              print "The existence of a nonstandard model suggests that the \
                    \induction hypothesis is not general enough or perhaps even \
                    \wrong. See the \"Inductive Properties\" section of the \
@@ -718,7 +712,7 @@
           | KK.Normal (sat_ps, unsat_js) =>
             let
               val (lib_ps, con_ps) =
-                List.partition (#liberal o snd o nth problems o fst) sat_ps
+                List.partition (#unsound o snd o nth problems o fst) sat_ps
             in
               update_checked_problems problems (unsat_js @ map fst lib_ps);
               if null con_ps then
@@ -735,9 +729,9 @@
                     (0, 0, donno)
                   else
                     let
-                      (* "co_js" is the list of conservative problems whose
-                         liberal pendants couldn't be satisfied and hence that
-                         most probably can't be satisfied themselves. *)
+                      (* "co_js" is the list of sound problems whose unsound
+                         pendants couldn't be satisfied and hence that most
+                         probably can't be satisfied themselves. *)
                       val co_js =
                         map (fn j => j - 1) unsat_js
                         |> filter (fn j =>
@@ -750,7 +744,7 @@
                       val problems =
                         problems |> filter_out_indices bye_js
                                  |> max_potential <= 0
-                                    ? filter_out (#liberal o snd)
+                                    ? filter_out (#unsound o snd)
                     in
                       solve_any_problem max_potential max_genuine donno false
                                         problems
@@ -770,7 +764,7 @@
                                                  (map fst sat_ps @ unsat_js)
                       val problems =
                         problems |> filter_out_indices bye_js
-                                 |> filter_out (#liberal o snd)
+                                 |> filter_out (#unsound o snd)
                     in solve_any_problem 0 max_genuine donno false problems end
                 end
             end
@@ -814,10 +808,10 @@
             ()
         (* scope * bool -> rich_problem list * bool
            -> rich_problem list * bool *)
-        fun add_problem_for_scope (scope as {datatypes, ...}, liberal)
+        fun add_problem_for_scope (scope as {datatypes, ...}, unsound)
                                   (problems, donno) =
           (check_deadline ();
-           case problem_for_scope liberal scope of
+           case problem_for_scope unsound scope of
              SOME problem =>
              (problems
               |> (null problems orelse
@@ -833,6 +827,28 @@
                ([], donno)
         val _ = Unsynchronized.change generated_problems (append problems)
         val _ = Unsynchronized.change generated_scopes (append scopes)
+        val _ =
+          if j + 1 = n then
+            let
+              val (unsound_problems, sound_problems) =
+                List.partition (#unsound o snd) (!generated_problems)
+            in
+              if not (null sound_problems) andalso
+                 forall (KK.is_problem_trivially_false o fst)
+                        sound_problems then
+                print_m (fn () =>
+                    "Warning: The conjecture either trivially holds or (more \
+                    \likely) lies outside Nitpick's supported fragment." ^
+                    (if exists (not o KK.is_problem_trivially_false o fst)
+                               unsound_problems then
+                       " Only potential counterexamples may be found."
+                     else
+                       ""))
+              else
+                ()
+            end
+          else
+            ()
       in
         solve_any_problem max_potential max_genuine donno true (rev problems)
       end
@@ -845,7 +861,7 @@
       let
         (* rich_problem list -> rich_problem list *)
         val do_filter =
-          if !met_potential = max_potential then filter_out (#liberal o snd)
+          if !met_potential = max_potential then filter_out (#unsound o snd)
           else I
         val total = length (!scopes)
         val unsat =
@@ -874,7 +890,7 @@
           if max_potential = original_max_potential then
             (print_m (fn () =>
                  "Nitpick found no " ^ das_wort_model ^ "." ^
-                 (if not standard andalso not (null induct_dataTs) then
+                 (if not standard andalso likely_in_struct_induct_step then
                     " This suggests that the induction hypothesis might be \
                     \general enough to prove this subgoal."
                   else
@@ -892,8 +908,8 @@
         end
 
     val (skipped, the_scopes) =
-      all_scopes hol_ctxt sym_break cards_assigns maxes_assigns iters_assigns
-                 bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
+      all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns
+                 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
     val _ = if skipped > 0 then
               print_m (fn () => "Too many scopes. Skipping " ^
                                 string_of_int skipped ^ " scope" ^
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -64,7 +64,7 @@
   val strip_any_connective : term -> term list * term
   val conjuncts_of : term -> term list
   val disjuncts_of : term -> term list
-  val unbit_and_unbox_type : typ -> typ
+  val unarize_and_unbox_type : typ -> typ
   val string_for_type : Proof.context -> typ -> string
   val prefix_name : string -> string -> string
   val shortest_name : string -> string
@@ -97,6 +97,7 @@
   val dest_n_tuple : int -> term -> term list
   val instantiate_type : theory -> typ -> typ -> typ -> typ
   val is_real_datatype : theory -> string -> bool
+  val is_standard_datatype : hol_context -> typ -> bool
   val is_quot_type : theory -> typ -> bool
   val is_codatatype : theory -> typ -> bool
   val is_pure_typedef : theory -> typ -> bool
@@ -116,11 +117,14 @@
   val is_sel : string -> bool
   val is_sel_like_and_no_discr : string -> bool
   val box_type : hol_context -> boxability -> typ -> typ
+  val binarize_nat_and_int_in_type : typ -> typ
+  val binarize_nat_and_int_in_term : term -> term
   val discr_for_constr : styp -> styp
   val num_sels_for_constr_type : typ -> int
   val nth_sel_name_for_constr_name : string -> int -> string
   val nth_sel_for_constr : styp -> int -> styp
-  val boxed_nth_sel_for_constr : hol_context -> styp -> int -> styp
+  val binarized_and_boxed_nth_sel_for_constr :
+    hol_context -> bool -> styp -> int -> styp
   val sel_no_from_name : string -> int
   val close_form : term -> term
   val eta_expand : typ list -> term -> int -> term
@@ -131,10 +135,11 @@
   val register_codatatype : typ -> string -> styp list -> theory -> theory
   val unregister_codatatype : typ -> theory -> theory
   val datatype_constrs : hol_context -> typ -> styp list
-  val boxed_datatype_constrs : hol_context -> typ -> styp list
+  val binarized_and_boxed_datatype_constrs :
+    hol_context -> bool -> typ -> styp list
   val num_datatype_constrs : hol_context -> typ -> int
   val constr_name_for_sel_like : string -> string
-  val boxed_constr_for_sel : hol_context -> styp -> styp
+  val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
   val discriminate_value : hol_context -> styp -> term -> term
   val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
   val construct_value : theory -> styp -> term list -> term
@@ -175,8 +180,8 @@
   val equational_fun_axioms : hol_context -> styp -> term list
   val is_equational_fun_surely_complete : hol_context -> styp -> bool
   val merge_type_vars_in_terms : term list -> term list
-  val ground_types_in_type : hol_context -> typ -> typ list
-  val ground_types_in_terms : hol_context -> term list -> typ list
+  val ground_types_in_type : hol_context -> bool -> typ -> typ list
+  val ground_types_in_terms : hol_context -> bool -> term list -> typ list
   val format_type : int list -> int list -> typ -> typ
   val format_term_type :
     theory -> const_table -> (term option * int list) list -> term -> typ
@@ -375,23 +380,23 @@
    (@{const_name ord_fun_inst.less_eq_fun}, 2)]
 
 (* typ -> typ *)
-fun unbit_type @{typ "unsigned_bit word"} = nat_T
-  | unbit_type @{typ "signed_bit word"} = int_T
-  | unbit_type @{typ bisim_iterator} = nat_T
-  | unbit_type (Type (s, Ts as _ :: _)) = Type (s, map unbit_type Ts)
-  | unbit_type T = T
-fun unbit_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
-    unbit_and_unbox_type (Type ("fun", Ts))
-  | unbit_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
-    Type ("*", map unbit_and_unbox_type Ts)
-  | unbit_and_unbox_type @{typ "unsigned_bit word"} = nat_T
-  | unbit_and_unbox_type @{typ "signed_bit word"} = int_T
-  | unbit_and_unbox_type @{typ bisim_iterator} = nat_T
-  | unbit_and_unbox_type (Type (s, Ts as _ :: _)) =
-    Type (s, map unbit_and_unbox_type Ts)
-  | unbit_and_unbox_type T = T
+fun unarize_type @{typ "unsigned_bit word"} = nat_T
+  | unarize_type @{typ "signed_bit word"} = int_T
+  | unarize_type @{typ bisim_iterator} = nat_T
+  | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
+  | unarize_type T = T
+fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
+    unarize_and_unbox_type (Type ("fun", Ts))
+  | unarize_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
+    Type ("*", map unarize_and_unbox_type Ts)
+  | unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
+  | unarize_and_unbox_type @{typ "signed_bit word"} = int_T
+  | unarize_and_unbox_type @{typ bisim_iterator} = nat_T
+  | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
+    Type (s, map unarize_and_unbox_type Ts)
+  | unarize_and_unbox_type T = T
 (* Proof.context -> typ -> string *)
-fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbit_and_unbox_type
+fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
 
 (* string -> string -> string *)
 val prefix_name = Long_Name.qualify o Long_Name.base_name
@@ -574,6 +579,10 @@
 (* theory -> string -> bool *)
 val is_typedef = is_some oo typedef_info
 val is_real_datatype = is_some oo Datatype.get_info
+(* hol_context -> typ -> bool *)
+fun is_standard_datatype ({thy, stds, ...} : hol_context) =
+  the o triple_lookup (type_match thy) stds
+
 (* theory -> typ -> bool *)
 fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
   | is_quot_type _ (Type ("FSet.fset", _)) = true
@@ -687,7 +696,7 @@
   member (op =) [@{const_name FunBox}, @{const_name PairBox},
                  @{const_name Quot}, @{const_name Zero_Rep},
                  @{const_name Suc_Rep}] s orelse
-  let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
+  let val (x as (s, T)) = (s, unarize_and_unbox_type T) in
     Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
     (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
     x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
@@ -698,7 +707,7 @@
   not (is_coconstr thy x)
 fun is_constr thy (x as (_, T)) =
   is_constr_like thy x andalso
-  not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) andalso
+  not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
   not (is_stale_constr thy x)
 (* string -> bool *)
 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
@@ -752,6 +761,15 @@
                            else InPair)) Ts)
   | _ => T
 
+(* typ -> typ *)
+fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
+  | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
+  | binarize_nat_and_int_in_type (Type (s, Ts)) =
+    Type (s, map binarize_nat_and_int_in_type Ts)
+  | binarize_nat_and_int_in_type T = T
+(* term -> term *)
+val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
+
 (* styp -> styp *)
 fun discr_for_constr (s, T) = (discr_prefix ^ s, body_type T --> bool_T)
 
@@ -768,9 +786,10 @@
   | nth_sel_for_constr (s, T) n =
     (nth_sel_name_for_constr_name s n,
      body_type T --> nth (maybe_curried_binder_types T) n)
-(* hol_context -> styp -> int -> styp *)
-fun boxed_nth_sel_for_constr hol_ctxt =
-  apsnd (box_type hol_ctxt InSel) oo nth_sel_for_constr
+(* hol_context -> bool -> styp -> int -> styp *)
+fun binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize =
+  apsnd ((binarize ? binarize_nat_and_int_in_type) o box_type hol_ctxt InSel)
+  oo nth_sel_for_constr
 
 (* string -> int *)
 fun sel_no_from_name s =
@@ -828,9 +847,8 @@
 fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
 fun suc_const T = Const (@{const_name Suc}, T --> T)
 
-(* hol_context -> typ -> styp list *)
-fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
-                              (T as Type (s, Ts)) =
+(* theory -> typ -> styp list *)
+fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
     (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
        SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
      | _ =>
@@ -843,8 +861,6 @@
              map (fn (s', Us) =>
                      (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
                           ---> T)) constrs
-             |> (triple_lookup (type_match thy) stds T |> the |> not) ?
-                cons (@{const_name NonStd}, @{typ \<xi>} --> T)
            end
          | NONE =>
            if is_record_type T then
@@ -867,15 +883,17 @@
          [])
   | uncached_datatype_constrs _ _ = []
 (* hol_context -> typ -> styp list *)
-fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
+fun datatype_constrs ({thy, constr_cache, ...} : hol_context) T =
   case AList.lookup (op =) (!constr_cache) T of
     SOME xs => xs
   | NONE =>
-    let val xs = uncached_datatype_constrs hol_ctxt T in
+    let val xs = uncached_datatype_constrs thy T in
       (Unsynchronized.change constr_cache (cons (T, xs)); xs)
     end
-fun boxed_datatype_constrs hol_ctxt =
-  map (apsnd (box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
+(* hol_context -> bool -> typ -> styp list *)
+fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
+  map (apsnd ((binarize ? binarize_nat_and_int_in_type)
+              o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
 (* hol_context -> typ -> int *)
 val num_datatype_constrs = length oo datatype_constrs
 
@@ -883,10 +901,12 @@
 fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
   | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
   | constr_name_for_sel_like s' = original_name s'
-(* hol_context -> styp -> styp *)
-fun boxed_constr_for_sel hol_ctxt (s', T') =
+(* hol_context -> bool -> styp -> styp *)
+fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
   let val s = constr_name_for_sel_like s' in
-    AList.lookup (op =) (boxed_datatype_constrs hol_ctxt (domain_type T')) s
+    AList.lookup (op =)
+        (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T'))
+        s
     |> the |> pair s
   end
 
@@ -957,10 +977,6 @@
       | _ => list_comb (Const x, args)
     end
 
-(* The higher this number is, the more nonstandard models can be generated. It's
-   not important enough to be a user option, though. *)
-val xi_card = 8
-
 (* (typ * int) list -> typ -> int *)
 fun card_of_type assigns (Type ("fun", [T1, T2])) =
     reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
@@ -970,7 +986,6 @@
   | card_of_type _ @{typ prop} = 2
   | card_of_type _ @{typ bool} = 2
   | card_of_type _ @{typ unit} = 1
-  | card_of_type _ @{typ \<xi>} = xi_card
   | card_of_type assigns T =
     case AList.lookup (op =) assigns T of
       SOME k => k
@@ -1027,7 +1042,6 @@
        | @{typ prop} => 2
        | @{typ bool} => 2
        | @{typ unit} => 1
-       | @{typ \<xi>} => xi_card
        | Type _ =>
          (case datatype_constrs hol_ctxt T of
             [] => if is_integer_type T orelse is_bit_type T then 0
@@ -1393,21 +1407,11 @@
 fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
   let
     val xs = datatype_constrs hol_ctxt dataT
-    val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs
-    val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
+    val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
+    val (xs', x) = split_last xs
   in
-    (if length xs = length xs' then
-       let
-         val (xs'', x) = split_last xs'
-       in
-         constr_case_body thy (1, x)
-         |> fold_rev (add_constr_case hol_ctxt res_T)
-                     (length xs' downto 2 ~~ xs'')
-       end
-     else
-       Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
-       |> fold_rev (add_constr_case hol_ctxt res_T)
-                   (length xs' downto 1 ~~ xs'))
+    constr_case_body thy (1, x)
+    |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
     |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   end
 
@@ -1738,10 +1742,11 @@
                                  (tac ctxt (auto_tac (clasimpset_of ctxt))))
        #> the #> Goal.finish ctxt) goal
 
-val max_cached_wfs = 100
-val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
-val cached_wf_props : (term * bool) list Unsynchronized.ref =
-  Unsynchronized.ref []
+val max_cached_wfs = 50
+val cached_timeout =
+  Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime)
+val cached_wf_props =
+  Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list)
 
 val termination_tacs = [Lexicographic_Order.lex_order_tac true,
                         ScnpReconstruct.sizechange_tac]
@@ -1772,19 +1777,20 @@
                  else
                    ()
        in
-         if tac_timeout = (!cached_timeout) andalso
-            length (!cached_wf_props) < max_cached_wfs then
+         if tac_timeout = Synchronized.value cached_timeout andalso
+            length (Synchronized.value cached_wf_props) < max_cached_wfs then
            ()
          else
-           (cached_wf_props := []; cached_timeout := tac_timeout);
-         case AList.lookup (op =) (!cached_wf_props) prop of
+           (Synchronized.change cached_wf_props (K []);
+            Synchronized.change cached_timeout (K tac_timeout));
+         case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of
            SOME wf => wf
          | NONE =>
            let
              val goal = prop |> cterm_of thy |> Goal.init
              val wf = exists (terminates_by ctxt tac_timeout goal)
                              termination_tacs
-           in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end
+           in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
        end)
     handle List.Empty => false
          | NO_TRIPLE () => false
@@ -1799,14 +1805,14 @@
     SOME (SOME b) => b
   | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
          case AList.lookup (op =) (!wf_cache) x of
-                  SOME (_, wf) => wf
-                | NONE =>
-                  let
-                    val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
-                    val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
-                  in
-                    Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
-                  end
+           SOME (_, wf) => wf
+         | NONE =>
+           let
+             val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
+             val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
+           in
+             Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
+           end
 
 (* typ list -> typ -> typ -> term -> term *)
 fun ap_curry [_] _ _ t = t
@@ -2025,29 +2031,33 @@
       | coalesce T = T
   in map (map_types (map_atyps coalesce)) ts end
 
-(* hol_context -> typ -> typ list -> typ list *)
-fun add_ground_types hol_ctxt T accum =
-  case T of
-    Type ("fun", Ts) => fold (add_ground_types hol_ctxt) Ts accum
-  | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
-  | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
-  | Type (_, Ts) =>
-    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} ::
-                      @{typ \<xi>} :: accum) T then
-      accum
-    else
-      T :: accum
-      |> fold (add_ground_types hol_ctxt)
-              (case boxed_datatype_constrs hol_ctxt T of
-                 [] => Ts
-               | xs => map snd xs)
-  | _ => insert (op =) T accum
+(* hol_context -> bool -> typ -> typ list -> typ list *)
+fun add_ground_types hol_ctxt binarize =
+  let
+    fun aux T accum =
+      case T of
+        Type ("fun", Ts) => fold aux Ts accum
+      | Type ("*", Ts) => fold aux Ts accum
+      | Type (@{type_name itself}, [T1]) => aux T1 accum
+      | Type (_, Ts) =>
+        if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum)
+                  T then
+          accum
+        else
+          T :: accum
+          |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt
+                                                                 binarize T of
+                         [] => Ts
+                       | xs => map snd xs)
+      | _ => insert (op =) T accum
+  in aux end
 
-(* hol_context -> typ -> typ list *)
-fun ground_types_in_type hol_ctxt T = add_ground_types hol_ctxt T []
+(* hol_context -> bool -> typ -> typ list *)
+fun ground_types_in_type hol_ctxt binarize T =
+  add_ground_types hol_ctxt binarize T []
 (* hol_context -> term list -> typ list *)
-fun ground_types_in_terms hol_ctxt ts =
-  fold (fold_types (add_ground_types hol_ctxt)) ts []
+fun ground_types_in_terms hol_ctxt binarize ts =
+  fold (fold_types (add_ground_types hol_ctxt binarize)) ts []
 
 (* theory -> const_table -> styp -> int list *)
 fun const_format thy def_table (x as (s, T)) =
@@ -2095,7 +2105,7 @@
 (* int list -> int list -> typ -> typ *)
 fun format_type default_format format T =
   let
-    val T = unbit_and_unbox_type T
+    val T = unarize_and_unbox_type T
     val format = format |> filter (curry (op <) 0)
   in
     if forall (curry (op =) 1) format then
@@ -2134,7 +2144,7 @@
            (* term -> term *)
            val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
            val (x' as (_, T'), js, ts) =
-             AList.find (op =) (!special_funs) (s, unbit_and_unbox_type T)
+             AList.find (op =) (!special_funs) (s, unarize_and_unbox_type T)
              |> the_single
            val max_j = List.last js
            val Ts = List.take (binder_types T', max_j + 1)
@@ -2224,7 +2234,7 @@
          let val t = Const (original_name s, T) in
            (t, format_term_type thy def_table formats t)
          end)
-      |>> map_types unbit_and_unbox_type
+      |>> map_types unarize_and_unbox_type
       |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
   in do_const end
 
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -33,10 +33,10 @@
   val merge_bounds : Kodkod.bound list -> Kodkod.bound list
   val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
   val declarative_axioms_for_datatypes :
-    hol_context -> int -> int Typtab.table -> kodkod_constrs
+    hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
     -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
   val kodkod_formula_from_nut :
-    int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
+    int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
 end;
 
 structure Nitpick_Kodkod : NITPICK_KODKOD =
@@ -317,7 +317,9 @@
              [ts] |> not exclusive ? cons (KK.TupleSet [])
            else
              [KK.TupleSet [],
-              if (* ### exclusive andalso*) T1 = T2 andalso epsilon > delta then
+              if T1 = T2 andalso epsilon > delta andalso
+                 (datatype_spec dtypes T1 |> the |> pairf #co #standard)
+                 = (false, true) then
                 index_seq delta (epsilon - delta)
                 |> map (fn j =>
                            KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
@@ -740,12 +742,14 @@
 (* nut NameTable.table -> styp -> KK.rel_expr *)
 fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
 
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-   -> styp -> int -> nfa_transition list *)
-fun nfa_transitions_for_sel hol_ctxt ({kk_project, ...} : kodkod_constrs)
-                            rel_table (dtypes : dtype_spec list) constr_x n =
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+   -> dtype_spec list -> styp -> int -> nfa_transition list *)
+fun nfa_transitions_for_sel hol_ctxt binarize
+                            ({kk_project, ...} : kodkod_constrs) rel_table
+                            (dtypes : dtype_spec list) constr_x n =
   let
-    val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt constr_x n
+    val x as (_, T) =
+      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
     val (r, R, arity) = const_triple rel_table x
     val type_schema = type_schema_of_rep T R
   in
@@ -754,61 +758,66 @@
                    else SOME (kk_project r (map KK.Num [0, j]), T))
                (index_seq 1 (arity - 1) ~~ tl type_schema)
   end
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-   -> styp -> nfa_transition list *)
-fun nfa_transitions_for_constr hol_ctxt kk rel_table dtypes (x as (_, T)) =
-  maps (nfa_transitions_for_sel hol_ctxt kk rel_table dtypes x)
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+   -> dtype_spec list -> styp -> nfa_transition list *)
+fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
+                               (x as (_, T)) =
+  maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
        (index_seq 0 (num_sels_for_constr_type T))
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-   -> dtype_spec -> nfa_entry option *)
-fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
-  | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
-  | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
-    SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
-                     o #const) constrs)
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+   -> dtype_spec list -> dtype_spec -> nfa_entry option *)
+fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
+  | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
+  | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
+  | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
+                           {typ, constrs, ...} =
+    SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table
+                                                dtypes o #const) constrs)
 
 val empty_rel = KK.Product (KK.None, KK.None)
 
 (* nfa_table -> typ -> typ -> KK.rel_expr list *)
-fun direct_path_rel_exprs nfa start final =
-  case AList.lookup (op =) nfa final of
-    SOME trans => map fst (filter (curry (op =) start o snd) trans)
+fun direct_path_rel_exprs nfa start_T final_T =
+  case AList.lookup (op =) nfa final_T of
+    SOME trans => map fst (filter (curry (op =) start_T o snd) trans)
   | NONE => []
 (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *)
-and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final =
-    fold kk_union (direct_path_rel_exprs nfa start final)
-         (if start = final then KK.Iden else empty_rel)
-  | any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final =
-    kk_union (any_path_rel_expr kk nfa qs start final)
-             (knot_path_rel_expr kk nfa qs start q final)
+and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
+                      final_T =
+    fold kk_union (direct_path_rel_exprs nfa start_T final_T)
+         (if start_T = final_T then KK.Iden else empty_rel)
+  | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T =
+    kk_union (any_path_rel_expr kk nfa Ts start_T final_T)
+             (knot_path_rel_expr kk nfa Ts start_T T final_T)
 (* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ
    -> KK.rel_expr *)
-and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start
-                       knot final =
-  kk_join (kk_join (any_path_rel_expr kk nfa qs knot final)
-                   (kk_reflexive_closure (loop_path_rel_expr kk nfa qs knot)))
-          (any_path_rel_expr kk nfa qs start knot)
+and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts
+                       start_T knot_T final_T =
+  kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T)
+                   (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T)))
+          (any_path_rel_expr kk nfa Ts start_T knot_T)
 (* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *)
-and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start =
-    fold kk_union (direct_path_rel_exprs nfa start start) empty_rel
-  | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (q :: qs) start =
-    if start = q then
-      kk_closure (loop_path_rel_expr kk nfa qs start)
+and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T =
+    fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel
+  | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts)
+                       start_T =
+    if start_T = T then
+      kk_closure (loop_path_rel_expr kk nfa Ts start_T)
     else
-      kk_union (loop_path_rel_expr kk nfa qs start)
-               (knot_path_rel_expr kk nfa qs start q start)
+      kk_union (loop_path_rel_expr kk nfa Ts start_T)
+               (knot_path_rel_expr kk nfa Ts start_T T start_T)
 
 (* nfa_table -> unit NfaGraph.T *)
 fun graph_for_nfa nfa =
   let
     (* typ -> unit NfaGraph.T -> unit NfaGraph.T *)
-    fun new_node q = perhaps (try (NfaGraph.new_node (q, ())))
+    fun new_node T = perhaps (try (NfaGraph.new_node (T, ())))
     (* nfa_table -> unit NfaGraph.T -> unit NfaGraph.T *)
     fun add_nfa [] = I
       | add_nfa ((_, []) :: nfa) = add_nfa nfa
-      | add_nfa ((q, ((_, q') :: transitions)) :: nfa) =
-        add_nfa ((q, transitions) :: nfa) o NfaGraph.add_edge (q, q') o
-        new_node q' o new_node q
+      | add_nfa ((T, ((_, T') :: transitions)) :: nfa) =
+        add_nfa ((T, transitions) :: nfa) o NfaGraph.add_edge (T, T') o
+        new_node T' o new_node T
   in add_nfa nfa NfaGraph.empty end
 
 (* nfa_table -> nfa_table list *)
@@ -816,27 +825,29 @@
   nfa |> graph_for_nfa |> NfaGraph.strong_conn
       |> map (fn keys => filter (member (op =) keys o fst) nfa)
 
-(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> KK.formula *)
-fun acyclicity_axiom_for_datatype dtypes kk nfa start =
+(* kodkod_constrs -> dtype_spec list -> nfa_table -> typ -> KK.formula *)
+fun acyclicity_axiom_for_datatype kk dtypes nfa start_T =
   #kk_no kk (#kk_intersect kk
-                 (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden)
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-   -> KK.formula list *)
-fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
-  map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
+                 (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
+   -> dtype_spec list -> KK.formula list *)
+fun acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes =
+  map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)
+             dtypes
   |> strongly_connected_sub_nfas
-  |> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst)
-                         nfa)
+  |> maps (fn nfa =>
+              map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa)
 
-(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
-   -> constr_spec -> int -> KK.formula *)
-fun sel_axiom_for_sel hol_ctxt j0
-        (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
+(* hol_context -> bool -> int -> kodkod_constrs -> nut NameTable.table
+   -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
+fun sel_axiom_for_sel hol_ctxt binarize j0
+        (kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
                 kk_join, ...}) rel_table dom_r
         ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
         n =
   let
-    val x as (_, T) = boxed_nth_sel_for_constr hol_ctxt const n
+    val x as (_, T) =
+      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
     val (r, R, arity) = const_triple rel_table x
     val R2 = dest_Func R |> snd
     val z = (epsilon - delta, delta + j0)
@@ -850,9 +861,9 @@
                               (kk_n_ary_function kk R2 r') (kk_no r'))
       end
   end
-(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
+(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
    -> constr_spec -> KK.formula list *)
-fun sel_axioms_for_constr hol_ctxt bits j0 kk rel_table
+fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table
         (constr as {const, delta, epsilon, explicit_max, ...}) =
   let
     val honors_explicit_max =
@@ -862,31 +873,31 @@
       [formula_for_bool honors_explicit_max]
     else
       let
-        val ran_r = discr_rel_expr rel_table const
+        val dom_r = discr_rel_expr rel_table const
         val max_axiom =
           if honors_explicit_max then
             KK.True
           else if is_twos_complement_representable bits (epsilon - delta) then
-            KK.LE (KK.Cardinality ran_r, KK.Num explicit_max)
+            KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
           else
             raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
                              "\"bits\" value " ^ string_of_int bits ^
                              " too small for \"max\"")
       in
         max_axiom ::
-        map (sel_axiom_for_sel hol_ctxt j0 kk rel_table ran_r constr)
+        map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr)
             (index_seq 0 (num_sels_for_constr_type (snd const)))
       end
   end
-(* hol_context -> int -> int -> kodkod_constrs -> nut NameTable.table
+(* hol_context -> bool -> int -> int -> kodkod_constrs -> nut NameTable.table
    -> dtype_spec -> KK.formula list *)
-fun sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table
+fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
                             ({constrs, ...} : dtype_spec) =
-  maps (sel_axioms_for_constr hol_ctxt bits j0 kk rel_table) constrs
+  maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
 
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> constr_spec
    -> KK.formula list *)
-fun uniqueness_axiom_for_constr hol_ctxt
+fun uniqueness_axiom_for_constr hol_ctxt binarize
         ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
          : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
   let
@@ -894,9 +905,10 @@
     fun conjunct_for_sel r =
       kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
     val num_sels = num_sels_for_constr_type (snd const)
-    val triples = map (const_triple rel_table
-                       o boxed_nth_sel_for_constr hol_ctxt const)
-                      (~1 upto num_sels - 1)
+    val triples =
+      map (const_triple rel_table
+           o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
+          (~1 upto num_sels - 1)
     val j0 = case triples |> hd |> #2 of
                Func (Atom (_, j0), _) => j0
              | R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr",
@@ -911,11 +923,11 @@
                   (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
                   (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
   end
-(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec
+(* hol_context -> bool -> kodkod_constrs -> nut NameTable.table -> dtype_spec
    -> KK.formula list *)
-fun uniqueness_axioms_for_datatype hol_ctxt kk rel_table
+fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
                                    ({constrs, ...} : dtype_spec) =
-  map (uniqueness_axiom_for_constr hol_ctxt kk rel_table) constrs
+  map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
 
 (* constr_spec -> int *)
 fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
@@ -932,25 +944,27 @@
        kk_disjoint_sets kk rs]
     end
 
-(* hol_context -> int -> int Typtab.table -> kodkod_constrs
+(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
    -> nut NameTable.table -> dtype_spec -> KK.formula list *)
-fun other_axioms_for_datatype _ _ _ _ _ {deep = false, ...} = []
-  | other_axioms_for_datatype hol_ctxt bits ofs kk rel_table
+fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []
+  | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table
                               (dtype as {typ, ...}) =
     let val j0 = offset_of_type ofs typ in
-      sel_axioms_for_datatype hol_ctxt bits j0 kk rel_table dtype @
-      uniqueness_axioms_for_datatype hol_ctxt kk rel_table dtype @
+      sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @
+      uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @
       partition_axioms_for_datatype j0 kk rel_table dtype
     end
 
-(* hol_context -> int -> int Typtab.table -> kodkod_constrs
+(* hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
    -> nut NameTable.table -> dtype_spec list -> KK.formula list *)
-fun declarative_axioms_for_datatypes hol_ctxt bits ofs kk rel_table dtypes =
-  acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
-  maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
+fun declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk rel_table
+                                     dtypes =
+  acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes @
+  maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
+       dtypes
 
-(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
-fun kodkod_formula_from_nut bits ofs liberal
+(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
+fun kodkod_formula_from_nut bits ofs
         (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
                 kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
                 kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -53,6 +53,9 @@
 val base_mixfix = "_\<^bsub>base\<^esub>"
 val step_mixfix = "_\<^bsub>step\<^esub>"
 val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
+val cyclic_co_val_name = "\<omega>"
+val cyclic_const_prefix = "\<xi>"
+val cyclic_type_name = nitpick_prefix ^ cyclic_const_prefix
 val opt_flag = nitpick_prefix ^ "opt"
 val non_opt_flag = nitpick_prefix ^ "non_opt"
 
@@ -88,7 +91,7 @@
     Const (nth_atom_name pool "" T j k, T)
 
 (* term -> real *)
-fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) =
+fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
     real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
   | extract_real_number t = real (snd (HOLogic.dest_number t))
 (* term * term -> order *)
@@ -107,23 +110,23 @@
   the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
 
 (* term -> term *)
-fun unbit_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
-    unbit_and_unbox_term t1
-  | unbit_and_unbox_term (Const (@{const_name PairBox},
-                          Type ("fun", [T1, Type ("fun", [T2, T3])]))
-                          $ t1 $ t2) =
-    let val Ts = map unbit_and_unbox_type [T1, T2] in
+fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
+    unarize_and_unbox_term t1
+  | unarize_and_unbox_term (Const (@{const_name PairBox},
+                                   Type ("fun", [T1, Type ("fun", [T2, T3])]))
+                            $ t1 $ t2) =
+    let val Ts = map unarize_and_unbox_type [T1, T2] in
       Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
-      $ unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
+      $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
     end
-  | unbit_and_unbox_term (Const (s, T)) = Const (s, unbit_and_unbox_type T)
-  | unbit_and_unbox_term (t1 $ t2) =
-    unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
-  | unbit_and_unbox_term (Free (s, T)) = Free (s, unbit_and_unbox_type T)
-  | unbit_and_unbox_term (Var (x, T)) = Var (x, unbit_and_unbox_type T)
-  | unbit_and_unbox_term (Bound j) = Bound j
-  | unbit_and_unbox_term (Abs (s, T, t')) =
-    Abs (s, unbit_and_unbox_type T, unbit_and_unbox_term t')
+  | unarize_and_unbox_term (Const (s, T)) = Const (s, unarize_and_unbox_type T)
+  | unarize_and_unbox_term (t1 $ t2) =
+    unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
+  | unarize_and_unbox_term (Free (s, T)) = Free (s, unarize_and_unbox_type T)
+  | unarize_and_unbox_term (Var (x, T)) = Var (x, unarize_and_unbox_type T)
+  | unarize_and_unbox_term (Bound j) = Bound j
+  | unarize_and_unbox_term (Abs (s, T, t')) =
+    Abs (s, unarize_and_unbox_type T, unarize_and_unbox_term t')
 
 (* typ -> typ -> (typ * typ) * (typ * typ) *)
 fun factor_out_types (T1 as Type ("*", [T11, T12]))
@@ -257,14 +260,13 @@
   | mk_tuple _ (t :: _) = t
   | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
 
-(* string * string * string * string -> scope -> nut list -> nut list
-   -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ -> typ -> rep
-   -> int list list -> term *)
-fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
-        ({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
-         : scope) sel_names rel_table bounds =
+(* bool -> atom_pool -> string * string * string * string -> scope -> nut list
+   -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
+   -> typ -> rep -> int list list -> term *)
+fun reconstruct_term unfold pool (maybe_name, base_name, step_name, abs_name)
+        ({hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits, datatypes,
+          ofs, ...} : scope) sel_names rel_table bounds =
   let
-    val pool = Unsynchronized.ref []
     val for_auto = (maybe_name = "")
     (* int list list -> int *)
     fun value_of_bits jss =
@@ -354,10 +356,10 @@
     fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
       ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
                  |> make_plain_fun maybe_opt T1 T2
-                 |> unbit_and_unbox_term
-                 |> typecast_fun (unbit_and_unbox_type T')
-                                 (unbit_and_unbox_type T1)
-                                 (unbit_and_unbox_type T2)
+                 |> unarize_and_unbox_term
+                 |> typecast_fun (unarize_and_unbox_type T')
+                                 (unarize_and_unbox_type T1)
+                                 (unarize_and_unbox_type T2)
     (* (typ * int) list -> typ -> typ -> int -> term *)
     fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
         let
@@ -397,13 +399,16 @@
         else case datatype_spec datatypes T of
           NONE => nth_atom pool for_auto T j k
         | SOME {deep = false, ...} => nth_atom pool for_auto T j k
-        | SOME {co, constrs, ...} =>
+        | SOME {co, standard, constrs, ...} =>
           let
             (* styp -> int list *)
             fun tuples_for_const (s, T) =
               tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
-            (* unit -> indexname * typ *)
-            fun var () = ((nth_atom_name pool "" T j k, 0), T)
+            (* unit -> term *)
+            fun cyclic_atom () =
+              nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
+            fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
+
             val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
                                  constrs
             val real_j = j + offset_of_type ofs T
@@ -413,8 +418,10 @@
                             else NONE)
                         (discr_jsss ~~ constrs) |> the
             val arg_Ts = curried_binder_types constr_T
-            val sel_xs = map (boxed_nth_sel_for_constr hol_ctxt constr_x)
-                             (index_seq 0 (length arg_Ts))
+            val sel_xs =
+              map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize
+                                                          constr_x)
+                  (index_seq 0 (length arg_Ts))
             val sel_Rs =
               map (fn x => get_first
                                (fn ConstName (s', T', R) =>
@@ -428,16 +435,18 @@
               map (map_filter (fn js => if hd js = real_j then SOME (tl js)
                                         else NONE)) sel_jsss
             val uncur_arg_Ts = binder_types constr_T
+            val maybe_cyclic = co orelse not standard
           in
-            if co andalso member (op =) seen (T, j) then
-              Var (var ())
+            if maybe_cyclic andalso not (null seen) andalso
+               member (op =) (seen |> unfold ? (fst o split_last)) (T, j) then
+              cyclic_var ()
             else if constr_s = @{const_name Word} then
               HOLogic.mk_number
                   (if T = @{typ "unsigned_bit word"} then nat_T else int_T)
                   (value_of_bits (the_single arg_jsss))
             else
               let
-                val seen = seen |> co ? cons (T, j)
+                val seen = seen |> maybe_cyclic ? cons (T, j)
                 val ts =
                   if length arg_Ts = 0 then
                     []
@@ -459,7 +468,7 @@
                            0 => mk_num 0
                          | n1 => case HOLogic.dest_number t2 |> snd of
                                    1 => mk_num n1
-                                 | n2 => Const (@{const_name Rings.divide},
+                                 | n2 => Const (@{const_name divide},
                                                 num_T --> num_T --> num_T)
                                          $ mk_num n1 $ mk_num n2)
                       | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
@@ -469,19 +478,25 @@
                           (is_abs_fun thy constr_x orelse
                            constr_s = @{const_name Quot}) then
                     Const (abs_name, constr_T) $ the_single ts
-                  else if not for_auto andalso
-                          constr_s = @{const_name NonStd} then
-                    Const (fst (dest_Const (the_single ts)), T)
                   else
                     list_comb (Const constr_x, ts)
               in
-                if co then
-                  let val var = var () in
-                    if exists_subterm (curry (op =) (Var var)) t then
-                      Const (@{const_name The}, (T --> bool_T) --> T)
-                      $ Abs ("\<omega>", T,
-                             Const (@{const_name "op ="}, T --> T --> bool_T)
-                             $ Bound 0 $ abstract_over (Var var, t))
+                if maybe_cyclic then
+                  let val var = cyclic_var () in
+                    if unfold andalso not standard andalso
+                       length seen = 1 andalso
+                       exists_subterm (fn Const (s, _) =>
+                                          String.isPrefix cyclic_const_prefix s
+                                        | t' => t' = var) t then
+                      subst_atomic [(var, cyclic_atom ())] t
+                    else if exists_subterm (curry (op =) var) t then
+                      if co then
+                        Const (@{const_name The}, (T --> bool_T) --> T)
+                        $ Abs (cyclic_co_val_name, T,
+                               Const (@{const_name "op ="}, T --> T --> bool_T)
+                               $ Bound 0 $ abstract_over (var, t))
+                      else
+                        cyclic_atom ()
                     else
                       t
                   end
@@ -537,17 +552,15 @@
         raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
                    Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
                    string_of_int (length jss))
-  in
-    polish_funs [] o unbit_and_unbox_term oooo term_for_rep []
-  end
+  in polish_funs [] o unarize_and_unbox_term oooo term_for_rep [] end
 
-(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
-   -> term *)
-fun term_for_name scope sel_names rel_table bounds name =
+(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
+   -> nut -> term *)
+fun term_for_name pool scope sel_names rel_table bounds name =
   let val T = type_of name in
     tuple_list_for_name rel_table bounds name
-    |> reconstruct_term ("", "", "", "") scope sel_names rel_table bounds T T
-                        (rep_of name)
+    |> reconstruct_term false pool ("", "", "", "") scope sel_names rel_table
+                        bounds T T (rep_of name)
   end
 
 (* Proof.context -> (string * string * string * string) * Proof.context *)
@@ -607,9 +620,10 @@
                        nondef_table, user_nondefs, simp_table, psimp_table,
                        intro_table, ground_thm_table, ersatz_table, skolems,
                        special_funs, unrolled_preds, wf_cache, constr_cache},
-         card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
+         binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
         formats all_frees free_names sel_names nonsel_names rel_table bounds =
   let
+    val pool = Unsynchronized.ref []
     val (wacky_names as (_, base_name, step_name, _), ctxt) =
       add_wacky_syntax ctxt
     val hol_ctxt =
@@ -626,14 +640,26 @@
        ersatz_table = ersatz_table, skolems = skolems,
        special_funs = special_funs, unrolled_preds = unrolled_preds,
        wf_cache = wf_cache, constr_cache = constr_cache}
-    val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
-                 bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
-                 ofs = ofs}
-    (* typ -> typ -> rep -> int list list -> term *)
-    val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table
-                                        bounds
-    (* nat -> typ -> nat -> typ *)
-    fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]]
+    val scope = {hol_ctxt = hol_ctxt, binarize = binarize,
+                 card_assigns = card_assigns, bits = bits,
+                 bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
+    (* bool -> typ -> typ -> rep -> int list list -> term *)
+    fun term_for_rep unfold =
+      reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
+    (* nat -> typ -> nat -> term *)
+    fun nth_value_of_type card T n =
+      let
+        (* bool -> term *)
+        fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]]
+      in
+        case aux false of
+          t as Const (s, _) =>
+          if String.isPrefix cyclic_const_prefix s then
+            HOLogic.mk_eq (t, aux true)
+          else
+            t
+        | t => t
+      end
     (* nat -> typ -> typ list *)
     fun all_values_of_type card T =
       index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord
@@ -653,7 +679,7 @@
         val (oper, (t1, T'), T) =
           case name of
             FreeName (s, T, _) =>
-            let val t = Free (s, unbit_and_unbox_type T) in
+            let val t = Free (s, unarize_and_unbox_type T) in
               ("=", (t, format_term_type thy def_table formats t), T)
             end
           | ConstName (s, T, _) =>
@@ -666,7 +692,7 @@
                    Const (@{const_name undefined}, T')
                  else
                    tuple_list_for_name rel_table bounds name
-                   |> term_for_rep T T' (rep_of name)
+                   |> term_for_rep false T T' (rep_of name)
       in
         Pretty.block (Pretty.breaks
             [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
@@ -675,14 +701,15 @@
     (* dtype_spec -> Pretty.T *)
     fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
       Pretty.block (Pretty.breaks
-          [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=",
+          [Syntax.pretty_typ ctxt (unarize_and_unbox_type typ), Pretty.str "=",
            Pretty.enum "," "{" "}"
                (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
                 (if complete then [] else [Pretty.str unrep]))])
     (* typ -> dtype_spec list *)
     fun integer_datatype T =
       [{typ = T, card = card_of_type card_assigns T, co = false,
-        complete = false, concrete = true, deep = true, constrs = []}]
+        standard = true, complete = false, concrete = true, deep = true,
+        constrs = []}]
       handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
     val (codatatypes, datatypes) =
       datatypes |> filter #deep |> List.partition #co
@@ -717,8 +744,8 @@
     val free_names =
       map (fn x as (s, T) =>
               case filter (curry (op =) x
-                           o pairf nickname_of (unbit_and_unbox_type o type_of))
-                          free_names of
+                       o pairf nickname_of (unarize_and_unbox_type o type_of))
+                       free_names of
                 [name] => name
               | [] => FreeName (s, T, Any)
               | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
@@ -758,7 +785,7 @@
     (* nut -> term *)
     fun free_name_assm name =
       HOLogic.mk_eq (Free (nickname_of name, type_of name),
-                     term_for_name scope sel_names rel_table bounds name)
+                     term_for_name pool scope sel_names rel_table bounds name)
     val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
     val model_assms = map free_name_assm free_names
     val assm = foldr1 s_conj (freeT_assms @ model_assms)
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -11,7 +11,7 @@
   type hol_context = Nitpick_HOL.hol_context
 
   val formulas_monotonic :
-    hol_context -> typ -> sign -> term list -> term list -> term -> bool
+    hol_context -> bool -> typ -> sign -> term list -> term list -> term -> bool
 end;
 
 structure Nitpick_Mono : NITPICK_MONO =
@@ -36,6 +36,7 @@
 
 type cdata =
   {hol_ctxt: hol_context,
+   binarize: bool,
    alpha_T: typ,
    max_fresh: int Unsynchronized.ref,
    datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
@@ -114,10 +115,10 @@
   | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
   | flatten_ctype C = [C]
 
-(* hol_context -> typ -> cdata *)
-fun initial_cdata hol_ctxt alpha_T =
-  ({hol_ctxt = hol_ctxt, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0,
-    datatype_cache = Unsynchronized.ref [],
+(* hol_context -> bool -> typ -> cdata *)
+fun initial_cdata hol_ctxt binarize alpha_T =
+  ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
+    max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
     constr_cache = Unsynchronized.ref []} : cdata)
 
 (* typ -> typ -> bool *)
@@ -278,9 +279,9 @@
                  AList.lookup (op =) (!constr_cache) x |> the)
   else
     fresh_ctype_for_type cdata T
-fun ctype_for_sel (cdata as {hol_ctxt, ...}) (x as (s, _)) =
-  x |> boxed_constr_for_sel hol_ctxt |> ctype_for_constr cdata
-    |> sel_ctype_from_constr_ctype s
+fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
+  x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
+    |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s
 
 (* literal list -> ctype -> ctype *)
 fun instantiate_ctype lits =
@@ -945,13 +946,14 @@
   map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
   |> cat_lines |> print_g
 
-(* hol_context -> typ -> sign -> term list -> term list -> term -> bool *)
-fun formulas_monotonic (hol_ctxt as {ctxt, ...}) alpha_T sn def_ts nondef_ts
-                       core_t =
+(* hol_context -> bool -> typ -> sign -> term list -> term list -> term
+   -> bool *)
+fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T sn def_ts
+                       nondef_ts core_t =
   let
     val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
                      Syntax.string_of_typ ctxt alpha_T)
-    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt alpha_T
+    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt binarize alpha_T
     val (gamma, cset) =
       (initial_gamma, slack)
       |> fold (consider_definitional_axiom cdata) def_ts
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -747,10 +747,10 @@
 
 (* scope -> styp -> int -> nut list * rep NameTable.table
    -> nut list * rep NameTable.table *)
-fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, ...}) (x as (_, T)) n
-                                      (vs, table) =
+fun choose_rep_for_nth_sel_for_constr (scope as {hol_ctxt, binarize, ...})
+                                      (x as (_, T)) n (vs, table) =
   let
-    val (s', T') = boxed_nth_sel_for_constr hol_ctxt x n
+    val (s', T') = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x n
     val R' = if n = ~1 orelse is_word_type (body_type T) orelse
                 (is_fun_type (range_type T') andalso
                  is_boolean_type (body_type T')) then
@@ -892,7 +892,7 @@
 (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
 fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
                                   bits, datatypes, ofs, ...})
-                       liberal table def =
+                       unsound table def =
   let
     val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
     (* polarity -> bool -> rep *)
@@ -1036,7 +1036,7 @@
               if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
               else opt_opt_case ()
           in
-            if liberal orelse polar = Neg orelse
+            if unsound orelse polar = Neg orelse
                is_concrete_type datatypes (type_of u1) then
               case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
                 (true, true) => opt_opt_case ()
@@ -1138,7 +1138,7 @@
               else
                 let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
                   if def orelse
-                     (liberal andalso (polar = Pos) = (oper = All)) orelse
+                     (unsound andalso (polar = Pos) = (oper = All)) orelse
                      is_complete_type datatypes (type_of u1) then
                     quant_u
                   else
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -9,7 +9,8 @@
 sig
   type hol_context = Nitpick_HOL.hol_context
   val preprocess_term :
-    hol_context -> term -> ((term list * term list) * (bool * bool)) * term
+    hol_context -> term
+    -> ((term list * term list) * (bool * bool)) * term * bool
 end
 
 structure Nitpick_Preproc : NITPICK_PREPROC =
@@ -54,15 +55,6 @@
   | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
   | should_use_binary_ints _ = false
 
-(* typ -> typ *)
-fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
-  | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
-  | binarize_nat_and_int_in_type (Type (s, Ts)) =
-    Type (s, map binarize_nat_and_int_in_type Ts)
-  | binarize_nat_and_int_in_type T = T
-(* term -> term *)
-val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
-
 (** Uncurrying **)
 
 (* theory -> term -> int Termtab.tab -> int Termtab.tab *)
@@ -517,8 +509,7 @@
         | (Const (x as (s, T)), args) =>
           let val arg_Ts = binder_types T in
             if length arg_Ts = length args andalso
-               (is_constr thy x orelse s = @{const_name Pair} orelse
-                x = (@{const_name Suc}, nat_T --> nat_T)) andalso
+               (is_constr thy x orelse s = @{const_name Pair}) andalso
                (not careful orelse not (is_Var t1) orelse
                 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
               discriminate_value hol_ctxt x t1 ::
@@ -1384,7 +1375,8 @@
 
 (** Preprocessor entry point **)
 
-(* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *)
+(* hol_context -> term
+   -> ((term list * term list) * (bool * bool)) * term * bool *)
 fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
                                   skolemize, uncurry, ...}) t =
   let
@@ -1425,7 +1417,7 @@
   in
     (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
       (got_all_mono_user_axioms, no_poly_user_axioms)),
-     do_rest false true core_t)
+     do_rest false true core_t, binarize)
   end
 
 end;
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -22,6 +22,7 @@
     typ: typ,
     card: int,
     co: bool,
+    standard: bool,
     complete: bool,
     concrete: bool,
     deep: bool,
@@ -29,6 +30,7 @@
 
   type scope = {
     hol_ctxt: hol_context,
+    binarize: bool,
     card_assigns: (typ * int) list,
     bits: int,
     bisim_depth: int,
@@ -47,7 +49,7 @@
   val scopes_equivalent : scope -> scope -> bool
   val scope_less_eq : scope -> scope -> bool
   val all_scopes :
-    hol_context -> int -> (typ option * int list) list
+    hol_context -> bool -> int -> (typ option * int list) list
     -> (styp option * int list) list -> (styp option * int list) list
     -> int list -> int list -> typ list -> typ list -> typ list
     -> int * scope list
@@ -71,6 +73,7 @@
   typ: typ,
   card: int,
   co: bool,
+  standard: bool,
   complete: bool,
   concrete: bool,
   deep: bool,
@@ -78,6 +81,7 @@
 
 type scope = {
   hol_ctxt: hol_context,
+  binarize: bool,
   card_assigns: (typ * int) list,
   bits: int,
   bisim_depth: int,
@@ -162,7 +166,7 @@
     fun miscs () =
       (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @
       (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
-       else ["bisim_depth = " ^ string_of_int bisim_depth])
+       else ["bisim_depth = " ^ signed_string_of_int bisim_depth])
   in
     setmp_show_all_types
         (fn () => (cards primary_card_assigns, cards secondary_card_assigns,
@@ -240,9 +244,10 @@
 
 val max_bits = 31 (* Kodkod limit *)
 
-(* hol_context -> (typ option * int list) list -> (styp option * int list) list
-   -> (styp option * int list) list -> int list -> int list -> typ -> block *)
-fun block_for_type (hol_ctxt as {thy, ...}) cards_assigns maxes_assigns
+(* hol_context -> bool -> (typ option * int list) list
+   -> (styp option * int list) list -> (styp option * int list) list -> int list
+   -> int list -> typ -> block *)
+fun block_for_type (hol_ctxt as {thy, ...}) binarize cards_assigns maxes_assigns
                    iters_assigns bitss bisim_depths T =
   if T = @{typ unsigned_bit} then
     [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
@@ -260,18 +265,18 @@
                                             (const_for_iterator_type T)))]
   else
     (Card T, lookup_type_ints_assign thy cards_assigns T) ::
-    (case datatype_constrs hol_ctxt T of
+    (case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
        [_] => []
      | constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
 
-(* hol_context -> (typ option * int list) list -> (styp option * int list) list
-   -> (styp option * int list) list -> int list -> int list -> typ list
-   -> typ list -> block list *)
-fun blocks_for_types hol_ctxt cards_assigns maxes_assigns iters_assigns bitss
-                     bisim_depths mono_Ts nonmono_Ts =
+(* hol_context -> bool -> (typ option * int list) list
+   -> (styp option * int list) list -> (styp option * int list) list -> int list
+   -> int list -> typ list -> typ list -> block list *)
+fun blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns iters_assigns
+                     bitss bisim_depths mono_Ts nonmono_Ts =
   let
     (* typ -> block *)
-    val block_for = block_for_type hol_ctxt cards_assigns maxes_assigns
+    val block_for = block_for_type hol_ctxt binarize cards_assigns maxes_assigns
                                    iters_assigns bitss bisim_depths
     val mono_block = maps block_for mono_Ts
     val nonmono_blocks = map block_for nonmono_Ts
@@ -312,10 +317,10 @@
 
 type scope_desc = (typ * int) list * (styp * int) list
 
-(* hol_context -> scope_desc -> typ * int -> bool *)
-fun is_surely_inconsistent_card_assign hol_ctxt (card_assigns, max_assigns)
-                                       (T, k) =
-  case datatype_constrs hol_ctxt T of
+(* hol_context -> bool -> scope_desc -> typ * int -> bool *)
+fun is_surely_inconsistent_card_assign hol_ctxt binarize
+                                       (card_assigns, max_assigns) (T, k) =
+  case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
     [] => false
   | xs =>
     let
@@ -328,21 +333,22 @@
         | effective_max card max = Int.min (card, max)
       val max = map2 effective_max dom_cards maxes |> Integer.sum
     in max < k end
-(* hol_context -> (typ * int) list -> (typ * int) list -> (styp * int) list
-   -> bool *)
-fun is_surely_inconsistent_scope_description hol_ctxt seen rest max_assigns =
-  exists (is_surely_inconsistent_card_assign hol_ctxt
+(* hol_context -> bool -> (typ * int) list -> (typ * int) list
+   -> (styp * int) list -> bool *)
+fun is_surely_inconsistent_scope_description hol_ctxt binarize seen rest
+                                             max_assigns =
+  exists (is_surely_inconsistent_card_assign hol_ctxt binarize
                                              (seen @ rest, max_assigns)) seen
 
-(* hol_context -> scope_desc -> (typ * int) list option *)
-fun repair_card_assigns hol_ctxt (card_assigns, max_assigns) =
+(* hol_context -> bool -> scope_desc -> (typ * int) list option *)
+fun repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) =
   let
     (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
     fun aux seen [] = SOME seen
       | aux seen ((T, 0) :: _) = NONE
       | aux seen ((T, k) :: rest) =
-        (if is_surely_inconsistent_scope_description hol_ctxt ((T, k) :: seen)
-                                                     rest max_assigns then
+        (if is_surely_inconsistent_scope_description hol_ctxt binarize
+                ((T, k) :: seen) rest max_assigns then
            raise SAME ()
          else
            case aux ((T, k) :: seen) rest of
@@ -373,13 +379,14 @@
 (* block -> scope_desc *)
 fun scope_descriptor_from_block block =
   fold_rev add_row_to_scope_descriptor block ([], [])
-(* hol_context -> block list -> int list -> scope_desc option *)
-fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) blocks columns =
+(* hol_context -> bool -> block list -> int list -> scope_desc option *)
+fun scope_descriptor_from_combination (hol_ctxt as {thy, ...}) binarize blocks
+                                      columns =
   let
     val (card_assigns, max_assigns) =
       maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
-    val card_assigns = repair_card_assigns hol_ctxt (card_assigns, max_assigns)
-                       |> the
+    val card_assigns =
+      repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) |> the
   in
     SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
           max_assigns)
@@ -460,13 +467,14 @@
     card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
   end
 
-(* hol_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
-fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) deep_dataTs
-                                        (desc as (card_assigns, _)) (T, card) =
+(* hol_context -> bool -> typ list -> scope_desc -> typ * int -> dtype_spec *)
+fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) binarize
+        deep_dataTs (desc as (card_assigns, _)) (T, card) =
   let
     val deep = member (op =) deep_dataTs T
     val co = is_codatatype thy T
-    val xs = boxed_datatype_constrs hol_ctxt T
+    val standard = is_standard_datatype hol_ctxt T
+    val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
     val self_recs = map (is_self_recursive_constr_type o snd) xs
     val (num_self_recs, num_non_self_recs) =
       List.partition I self_recs |> pairself length
@@ -481,8 +489,8 @@
                                 num_non_self_recs)
                (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
   in
-    {typ = T, card = card, co = co, complete = complete, concrete = concrete,
-     deep = deep, constrs = constrs}
+    {typ = T, card = card, co = co, standard = standard, complete = complete,
+     concrete = concrete, deep = deep, constrs = constrs}
   end
 
 (* int -> int *)
@@ -493,21 +501,21 @@
     min_bits_for_nat_value (fold Integer.max
         (map snd card_assigns @ map snd max_assigns) 0)
 
-(* hol_context -> int -> typ list -> scope_desc -> scope *)
-fun scope_from_descriptor (hol_ctxt as {thy, ...}) sym_break deep_dataTs
-                          (desc as (card_assigns, _)) =
+(* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
+fun scope_from_descriptor (hol_ctxt as {thy, ...}) binarize sym_break
+                          deep_dataTs (desc as (card_assigns, _)) =
   let
     val datatypes =
-      map (datatype_spec_from_scope_descriptor hol_ctxt deep_dataTs desc)
-          (filter (is_datatype thy o fst) card_assigns)
+      map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
+               desc) (filter (is_datatype thy o fst) card_assigns)
     val bits = card_of_type card_assigns @{typ signed_bit} - 1
                handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
                       card_of_type card_assigns @{typ unsigned_bit}
                       handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
     val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
   in
-    {hol_ctxt = hol_ctxt, card_assigns = card_assigns, datatypes = datatypes,
-     bits = bits, bisim_depth = bisim_depth,
+    {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
+     datatypes = datatypes, bits = bits, bisim_depth = bisim_depth,
      ofs = if sym_break <= 0 then Typtab.empty
            else offset_table_for_card_assigns thy card_assigns datatypes}
   end
@@ -517,7 +525,7 @@
 fun repair_cards_assigns_wrt_boxing _ _ [] = []
   | repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
     (if is_fun_type T orelse is_pair_type T then
-       Ts |> filter (curry (type_match thy o swap) T o unbit_and_unbox_type)
+       Ts |> filter (curry (type_match thy o swap) T o unarize_and_unbox_type)
           |> map (rpair ks o SOME)
      else
        [(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns
@@ -527,26 +535,29 @@
 val max_scopes = 4096
 val distinct_threshold = 512
 
-(* hol_context -> int -> (typ option * int list) list
+(* hol_context -> bool -> int -> (typ option * int list) list
    -> (styp option * int list) list -> (styp option * int list) list -> int list
    -> typ list -> typ list -> typ list -> int * scope list *)
-fun all_scopes (hol_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
-               iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs =
+fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns
+               maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
+               deep_dataTs =
   let
     val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
                                                         cards_assigns
-    val blocks = blocks_for_types hol_ctxt cards_assigns maxes_assigns
+    val blocks = blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns
                                   iters_assigns bitss bisim_depths mono_Ts
                                   nonmono_Ts
     val ranks = map rank_of_block blocks
     val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
     val head = take max_scopes all
-    val descs = map_filter (scope_descriptor_from_combination hol_ctxt blocks)
-                           head
+    val descs =
+      map_filter (scope_descriptor_from_combination hol_ctxt binarize blocks)
+                 head
   in
     (length all - length head,
      descs |> length descs <= distinct_threshold ? distinct (op =)
-           |> map (scope_from_descriptor hol_ctxt sym_break deep_dataTs))
+           |> map (scope_from_descriptor hol_ctxt binarize sym_break
+                                         deep_dataTs))
   end
 
 end;
diff -r 3b9762ad372d -r a815c3f4eef2 src/HOL/Tools/Nitpick/nitpick_tests.ML
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Wed Feb 17 11:31:15 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Wed Feb 17 21:13:40 2010 +0100
@@ -308,7 +308,7 @@
                        NameTable.empty
     val u = Op1 (Not, type_of u, rep_of u, u)
             |> rename_vars_in_nut pool table
-    val formula = kodkod_formula_from_nut bits Typtab.empty false constrs u
+    val formula = kodkod_formula_from_nut bits Typtab.empty constrs u
     val bounds = map (bound_for_plain_rel ctxt debug) free_rels
     val univ_card = univ_card nat_card int_card j0 bounds formula
     val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)