# HG changeset patch
# User blanchet
# Date 1268123123 -3600
# Node ID ff2bf50505aba3d34980168eae9eebf8c229c733
# Parent  fee01e85605ff694e11f2d01d18b8e571bd477ea
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"

diff -r fee01e85605f -r ff2bf50505ab doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Mar 08 15:20:40 2010 -0800
+++ b/doc-src/Nitpick/nitpick.tex	Tue Mar 09 09:25:23 2010 +0100
@@ -136,8 +136,8 @@
 suggesting several textual improvements.
 % and Perry James for reporting a typo.
 
-\section{First Steps}
-\label{first-steps}
+\section{Overview}
+\label{overview}
 
 This section introduces Nitpick by presenting small examples. If possible, you
 should try out the examples on your workstation. Your theory file should start
@@ -145,7 +145,7 @@
 
 \prew
 \textbf{theory}~\textit{Scratch} \\
-\textbf{imports}~\textit{Main~Coinductive\_List~Quotient\_Product~RealDef} \\
+\textbf{imports}~\textit{Main~Quotient\_Product~RealDef} \\
 \textbf{begin}
 \postw
 
@@ -677,7 +677,7 @@
 \hbox{}\qquad\qquad $y = \Abs{(1,\, 0)}$ \\
 \hbox{}\qquad Datatypes: \\
 \hbox{}\qquad\qquad $\textit{nat} = \{0,\, 1,\, \unr\}$ \\
-\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat} = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
+\hbox{}\qquad\qquad $\textit{nat} \times \textit{nat}~[\textsl{boxed\/}] = \{(0,\, 0),\> (1,\, 0),\> \unr\}$ \\
 \hbox{}\qquad\qquad $\textit{my\_int} = \{\Abs{(0,\, 0)},\> \Abs{(1,\, 0)},\> \unr\}$
 \postw
 
@@ -704,8 +704,6 @@
 & \lparr\textit{Xcoord} = 1,\> \textit{Ycoord} = 1\rparr,\, \unr\}\end{aligned}$
 \postw
 
-
-
 Finally, Nitpick provides rudimentary support for rationals and reals using a
 similar approach:
 
@@ -940,9 +938,10 @@
 \label{coinductive-datatypes}
 
 While Isabelle regrettably lacks a high-level mechanism for defining coinductive
-datatypes, the \textit{Coinductive\_List} theory provides a coinductive ``lazy
-list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick supports
-these lazy lists seamlessly and provides a hook, described in
+datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's
+\textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive
+``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick
+supports these lazy lists seamlessly and provides a hook, described in
 \S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
 datatypes.
 
@@ -1165,10 +1164,11 @@
 
 {\looseness=-1
 Boxing can be enabled or disabled globally or on a per-type basis using the
-\textit{box} option. Moreover, setting the cardinality of a function or
-product type implicitly enables boxing for that type. Nitpick usually performs
-reasonable choices about which types should be boxed, but option tweaking
-sometimes helps.
+\textit{box} option. Nitpick usually performs reasonable choices about which
+types should be boxed, but option tweaking sometimes helps. A related optimization,
+``finalization,'' attempts to wrap functions that constant at all but finitely
+many points (e.g., finite sets); see the documentation for the \textit{finalize}
+option in \S\ref{scope-of-search} for details.
 
 }
 
@@ -1850,7 +1850,7 @@
 The number of options can be overwhelming at first glance. Do not let that worry
 you: Nitpick's defaults have been chosen so that it almost always does the right
 thing, and the most important options have been covered in context in
-\S\ref{first-steps}.
+\S\ref{overview}.
 
 The descriptions below refer to the following syntactic quantities:
 
@@ -1936,14 +1936,10 @@
 Specifies the sequence of cardinalities to use for a given type.
 For free types, and often also for \textbf{typedecl}'d types, it usually makes
 sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
-Although function and product types are normally mapped directly to the
-corresponding Kodkod concepts, setting
-the cardinality of such types is also allowed and implicitly enables ``boxing''
-for them, as explained in the description of the \textit{box}~\qty{type}
-and \textit{box} (\S\ref{scope-of-search}) options.
 
 \nopagebreak
-{\small See also \textit{mono} (\S\ref{scope-of-search}).}
+{\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
+(\S\ref{scope-of-search}).}
 
 \opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
 Specifies the default sequence of cardinalities to use. This can be overridden
@@ -2062,8 +2058,8 @@
 Specifies whether Nitpick should attempt to wrap (``box'') a given function or
 product type in an isomorphic datatype internally. Boxing is an effective mean
 to reduce the search space and speed up Nitpick, because the isomorphic datatype
-is approximated by a subset of the possible function or pair values;
-like other drastic optimizations, it can also prevent the discovery of
+is approximated by a subset of the possible function or pair values.
+Like other drastic optimizations, it can also prevent the discovery of
 counterexamples. The option can take the following values:
 
 \begin{enum}
@@ -2075,30 +2071,68 @@
 higher-order functions are good candidates for boxing.
 \end{enum}
 
-Setting the \textit{card}~\qty{type} option for a function or product type
-implicitly enables boxing for that type.
-
 \nopagebreak
-{\small See also \textit{verbose} (\S\ref{output-format})
-and \textit{debug} (\S\ref{output-format}).}
+{\small See also \textit{finitize} (\S\ref{scope-of-search}), \textit{verbose}
+(\S\ref{output-format}), and \textit{debug} (\S\ref{output-format}).}
 
 \opsmart{box}{dont\_box}
 Specifies the default boxing setting to use. This can be overridden on a
 per-type basis using the \textit{box}~\qty{type} option described above.
 
+\opargboolorsmart{finitize}{type}{dont\_finitize}
+Specifies whether Nitpick should attempt to finitize a given type, which can be
+a function type or an infinite ``shallow datatype'' (an infinite datatype whose
+constructors don't appear in the problem).
+
+For function types, Nitpick performs a monotonicity analysis to detect functions
+that are constant at all but finitely many points (e.g., finite sets) and treats
+such occurrences specially, thereby increasing the precision. The option can
+then take the following values:
+
+\begin{enum}
+\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the type.
+\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}}: Finitize the
+type wherever possible.
+\end{enum}
+
+The semantics of the option is somewhat different for infinite shallow
+datatypes:
+
+\begin{enum}
+\item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is
+unsound, counterexamples generated under these conditions are tagged as ``likely
+genuine.''
+\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype.
+\item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to
+detect whether the datatype can be safely finitized before finitizing it.
+\end{enum}
+
+Like other drastic optimizations, finitization can sometimes prevent the
+discovery of counterexamples.
+
+\nopagebreak
+{\small See also \textit{box} (\S\ref{scope-of-search}), \textit{mono}
+(\S\ref{scope-of-search}), \textit{verbose} (\S\ref{output-format}), and
+\textit{debug} (\S\ref{output-format}).}
+
+\opsmart{finitize}{dont\_finitize}
+Specifies the default finitization setting to use. This can be overridden on a
+per-type basis using the \textit{finitize}~\qty{type} option described above.
+
 \opargboolorsmart{mono}{type}{non\_mono}
-Specifies whether the given type should be considered monotonic when
-enumerating scopes. If the option is set to \textit{smart}, Nitpick performs a
-monotonicity check on the type. Setting this option to \textit{true} can reduce
-the number of scopes tried, but it also diminishes the theoretical chance of
+Specifies whether the given type should be considered monotonic when enumerating
+scopes and finitizing types. If the option is set to \textit{smart}, Nitpick
+performs a monotonicity check on the type. Setting this option to \textit{true}
+can reduce the number of scopes tried, but it can also diminish the chance of
 finding a counterexample, as demonstrated in \S\ref{scope-monotonicity}.
 
 \nopagebreak
 {\small See also \textit{card} (\S\ref{scope-of-search}),
+\textit{finitize} (\S\ref{scope-of-search}),
 \textit{merge\_type\_vars} (\S\ref{scope-of-search}), and \textit{verbose}
 (\S\ref{output-format}).}
 
-\opsmart{mono}{non\_box}
+\opsmart{mono}{non\_mono}
 Specifies the default monotonicity setting to use. This can be overridden on a
 per-type basis using the \textit{mono}~\qty{type} option described above.
 
diff -r fee01e85605f -r ff2bf50505ab doc-src/manual.bib
--- a/doc-src/manual.bib	Mon Mar 08 15:20:40 2010 -0800
+++ b/doc-src/manual.bib	Tue Mar 09 09:25:23 2010 +0100
@@ -1759,3 +1759,12 @@
   key = "Wikipedia",
   title = "Wikipedia: {AA} Tree",
   note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}
+
+@incollection{lochbihler-2010,
+  title = "Coinduction",
+  author = "Andreas Lochbihler",
+  booktitle = "The Archive of Formal Proofs",
+  editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
+  publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
+  month = "Feb.",
+  year = 2010}
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Nitpick.thy	Tue Mar 09 09:25:23 2010 +0100
@@ -38,8 +38,9 @@
            and Quot :: "'a \<Rightarrow> 'b"
            and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
 
+datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
+datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
 datatype ('a, 'b) pair_box = PairBox 'a 'b
-datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
 
 typedecl unsigned_bit
 typedecl signed_bit
@@ -220,8 +221,8 @@
 use "Tools/Nitpick/kodkod_sat.ML"
 use "Tools/Nitpick/nitpick_util.ML"
 use "Tools/Nitpick/nitpick_hol.ML"
+use "Tools/Nitpick/nitpick_mono.ML"
 use "Tools/Nitpick/nitpick_preproc.ML"
-use "Tools/Nitpick/nitpick_mono.ML"
 use "Tools/Nitpick/nitpick_scope.ML"
 use "Tools/Nitpick/nitpick_peephole.ML"
 use "Tools/Nitpick/nitpick_rep.ML"
@@ -236,11 +237,12 @@
 setup {* Nitpick_Isar.setup *}
 
 hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
-    bisim_iterator_max Quot 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
+    bisim_iterator_max Quot Tha FinFun FunBox PairBox 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 word
+hide (open) type bisim_iterator fin_fun fun_box pair_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 fee01e85605f -r ff2bf50505ab src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Mar 09 09:25:23 2010 +0100
@@ -8,7 +8,7 @@
 header {* Examples from the Nitpick Manual *}
 
 theory Manual_Nits
-imports Main Coinductive_List Quotient_Product RealDef
+imports Main Quotient_Product RealDef
 begin
 
 chapter {* 3. First Steps *}
@@ -173,13 +173,35 @@
 
 subsection {* 3.9. Coinductive Datatypes *}
 
+(* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
+we cannot rely on its presence, we expediently provide our own axiomatization.
+The examples also work unchanged with Lochbihler's "Coinductive_List" theory. *)
+
+typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
+
+definition LNil where "LNil = Abs_llist (Inl [])"
+definition LCons where
+"LCons y ys = Abs_llist (case Rep_llist ys of
+                           Inl ys' \<Rightarrow> Inl (y # ys')
+                         | Inr f \<Rightarrow> Inr (\<lambda>n. case n of 0 \<Rightarrow> y | Suc m \<Rightarrow> f m))"
+
+axiomatization iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
+
+lemma iterates_def [nitpick_simp]:
+"iterates f a = LCons a (iterates f (f a))"
+sorry
+
+setup {*
+Nitpick.register_codatatype @{typ "'a llist"} ""
+    (map dest_Const [@{term LNil}, @{term LCons}])
+*}
+
 lemma "xs \<noteq> LCons a xs"
 nitpick
 oops
 
 lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
 nitpick [verbose]
-nitpick [bisim_depth = -1, verbose]
 oops
 
 lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -36,8 +36,10 @@
 datatype rep = SRep | RRep
 
 (* Proof.context -> typ -> unit *)
-fun check_type ctxt (Type ("fun", Ts)) = List.app (check_type ctxt) Ts
-  | check_type ctxt (Type ("*", Ts)) = List.app (check_type ctxt) Ts
+fun check_type ctxt (Type (@{type_name fun}, Ts)) =
+    List.app (check_type ctxt) Ts
+  | check_type ctxt (Type (@{type_name "*"}, Ts)) =
+    List.app (check_type ctxt) Ts
   | check_type _ @{typ bool} = ()
   | check_type _ (TFree (_, @{sort "{}"})) = ()
   | check_type _ (TFree (_, @{sort HOL.type})) = ()
@@ -45,13 +47,14 @@
     raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
 
 (* rep -> (typ -> int) -> typ -> int list *)
-fun atom_schema_of SRep card (Type ("fun", [T1, T2])) =
+fun atom_schema_of SRep card (Type (@{type_name fun}, [T1, T2])) =
     replicate_list (card T1) (atom_schema_of SRep card T2)
-  | atom_schema_of RRep card (Type ("fun", [T1, @{typ bool}])) =
+  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
     atom_schema_of SRep card T1
-  | atom_schema_of RRep card (Type ("fun", [T1, T2])) =
+  | atom_schema_of RRep card (Type (@{type_name fun}, [T1, T2])) =
     atom_schema_of SRep card T1 @ atom_schema_of RRep card T2
-  | atom_schema_of _ card (Type ("*", Ts)) = maps (atom_schema_of SRep card) Ts
+  | atom_schema_of _ card (Type (@{type_name "*"}, Ts)) =
+    maps (atom_schema_of SRep card) Ts
   | atom_schema_of _ card T = [card T]
 (* rep -> (typ -> int) -> typ -> int *)
 val arity_of = length ooo atom_schema_of
@@ -89,7 +92,7 @@
 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 =
+    fun R_rep_from_S_rep (T as Type (@{type_name fun}, [T1, @{typ bool}])) r =
         let
           val jss = atom_schema_of SRep card T1 |> map (rpair 0)
                     |> all_combinations
@@ -100,7 +103,7 @@
                (index_seq 0 (length jss)) jss
           |> foldl1 Union
         end
-      | R_rep_from_S_rep (Type ("fun", [T1, T2])) r =
+      | R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
         let
           val jss = atom_schema_of SRep card T1 |> map (rpair 0)
                     |> all_combinations
@@ -115,7 +118,7 @@
         end
       | R_rep_from_S_rep _ r = r
     (* typ list -> typ -> rel_expr -> rel_expr *)
-    fun S_rep_from_R_rep Ts (T as Type ("fun", _)) r =
+    fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
         Comprehension (decls_for SRep card Ts T,
             RelEq (R_rep_from_S_rep T
                        (rel_expr_for_bound_var card SRep (T :: Ts) 0), r))
@@ -137,7 +140,9 @@
        | Const (@{const_name "op ="}, _) $ t1 $ t2 =>
          RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
        | Const (@{const_name ord_class.less_eq},
-                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
+                Type (@{type_name fun},
+                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+         $ t1 $ t2 =>
          Subset (to_R_rep Ts t1, to_R_rep Ts t2)
        | @{const "op &"} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
        | @{const "op |"} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
@@ -179,7 +184,8 @@
        | Const (@{const_name "op ="}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name "op ="}, _) => to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name ord_class.less_eq},
-                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>
+                Type (@{type_name fun},
+                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
          to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name ord_class.less_eq}, _) =>
          to_R_rep Ts (eta_expand Ts t 2)
@@ -190,7 +196,7 @@
        | @{const "op -->"} $ _ => to_R_rep Ts (eta_expand Ts t 1)
        | @{const "op -->"} => to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name bot_class.bot},
-                T as Type ("fun", [_, @{typ bool}])) =>
+                T as Type (@{type_name fun}, [_, @{typ bool}])) =>
          empty_n_ary_rel (arity_of RRep card T)
        | Const (@{const_name insert}, _) $ t1 $ t2 =>
          Union (to_S_rep Ts t1, to_R_rep Ts t2)
@@ -203,27 +209,35 @@
            raise NOT_SUPPORTED "transitive closure for function or pair type"
        | Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name semilattice_inf_class.inf},
-                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
+                Type (@{type_name fun},
+                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+         $ t1 $ t2 =>
          Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
        | Const (@{const_name semilattice_inf_class.inf}, _) $ _ =>
          to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name semilattice_inf_class.inf}, _) =>
          to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name semilattice_sup_class.sup},
-                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
+                Type (@{type_name fun},
+                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+         $ t1 $ t2 =>
          Union (to_R_rep Ts t1, to_R_rep Ts t2)
        | Const (@{const_name semilattice_sup_class.sup}, _) $ _ =>
          to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name semilattice_sup_class.sup}, _) =>
          to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name minus_class.minus},
-                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ t1 $ t2 =>
+                Type (@{type_name fun},
+                      [Type (@{type_name fun}, [_, @{typ bool}]), _]))
+         $ t1 $ t2 =>
          Difference (to_R_rep Ts t1, to_R_rep Ts t2)
        | Const (@{const_name minus_class.minus},
-                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) $ _ =>
+                Type (@{type_name fun},
+                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
          to_R_rep Ts (eta_expand Ts t 1)
        | Const (@{const_name minus_class.minus},
-                Type ("fun", [Type ("fun", [_, @{typ bool}]), _])) =>
+                Type (@{type_name fun},
+                      [Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
          to_R_rep Ts (eta_expand Ts t 2)
        | Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
        | Const (@{const_name Pair}, _) $ _ => raise SAME ()
@@ -277,7 +291,8 @@
   end
 
 (* (typ -> int) -> typ list -> typ -> rel_expr -> formula *)
-fun declarative_axiom_for_rel_expr card Ts (Type ("fun", [T1, T2])) r =
+fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
+                                   r =
     if body_type T2 = bool_T then
       True
     else
@@ -294,8 +309,9 @@
   let
     val thy = ProofContext.theory_of ctxt
     (* typ -> int *)
-    fun card (Type ("fun", [T1, T2])) = reasonable_power (card T2) (card T1)
-      | card (Type ("*", [T1, T2])) = card T1 * card T2
+    fun card (Type (@{type_name fun}, [T1, T2])) =
+        reasonable_power (card T2) (card T1)
+      | card (Type (@{type_name "*"}, [T1, T2])) = card T1 * card T2
       | card @{typ bool} = 2
       | card T = Int.max (1, raw_card T)
     val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -15,6 +15,7 @@
     bitss: int list,
     bisim_depths: int list,
     boxes: (typ option * bool option) list,
+    finitizes: (typ option * bool option) list,
     monos: (typ option * bool option) list,
     stds: (typ option * bool) list,
     wfs: (styp option * bool option) list,
@@ -87,6 +88,7 @@
   bitss: int list,
   bisim_depths: int list,
   boxes: (typ option * bool option) list,
+  finitizes: (typ option * bool option) list,
   monos: (typ option * bool option) list,
   stds: (typ option * bool) list,
   wfs: (styp option * bool option) list,
@@ -200,13 +202,13 @@
             error "You must import the theory \"Nitpick\" to use Nitpick"
 *)
     val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
-         boxes, monos, stds, wfs, sat_solver, falsify, debug, verbose, overlord,
-         user_axioms, assms, merge_type_vars, binary_ints, destroy_constrs,
-         specialize, skolemize, star_linear_preds, uncurry, fast_descrs,
-         peephole_optim, tac_timeout, sym_break, sharing_depth, flatten_props,
-         max_threads, show_skolems, show_datatypes, show_consts, evals, formats,
-         max_potential, max_genuine, check_potential, check_genuine, batch_size,
-         ...} =
+         boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
+         verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
+         destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
+         fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
+         flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
+         evals, formats, max_potential, max_genuine, check_potential,
+         check_genuine, batch_size, ...} =
       params
     val state_ref = Unsynchronized.ref state
     (* Pretty.T -> unit *)
@@ -289,7 +291,7 @@
     val _ = null (Term.add_tvars assms_t []) orelse
             raise NOT_SUPPORTED "schematic type variables"
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
-         binarize) = preprocess_term hol_ctxt assms_t
+         binarize) = preprocess_term hol_ctxt finitizes monos assms_t
     val got_all_user_axioms =
       got_all_mono_user_axioms andalso no_poly_user_axioms
 
@@ -321,7 +323,11 @@
       fold add_free_and_const_names (nondef_us @ def_us) ([], [])
     val (sel_names, nonsel_names) =
       List.partition (is_sel o nickname_of) const_names
-    val genuine_means_genuine = got_all_user_axioms andalso none_true wfs
+    val sound_finitizes =
+      none_true (filter_out (fn (SOME (Type (@{type_name fun}, _)), _) => true
+                          | _ => false) finitizes)
+    val genuine_means_genuine =
+      got_all_user_axioms andalso none_true wfs andalso sound_finitizes
     val standard = forall snd stds
 (*
     val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
@@ -340,21 +346,30 @@
         ". " ^ extra
       end
     (* typ -> bool *)
-    fun is_type_always_monotonic T =
+    fun is_type_fundamentally_monotonic T =
       (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
        (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
       is_number_type thy T orelse is_bit_type T
     fun is_type_actually_monotonic T =
       formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
+    fun is_type_kind_of_monotonic T =
+      case triple_lookup (type_match thy) monos T of
+        SOME (SOME false) => false
+      | _ => is_type_actually_monotonic T
     fun is_type_monotonic T =
       unique_scope orelse
       case triple_lookup (type_match thy) monos T of
         SOME (SOME b) => b
-      | _ => is_type_always_monotonic T orelse is_type_actually_monotonic T
-    fun is_type_finitizable T =
-      case triple_lookup (type_match thy) monos T of
-        SOME (SOME false) => false
-      | _ => is_type_actually_monotonic T
+      | _ => is_type_fundamentally_monotonic T orelse
+             is_type_actually_monotonic T
+    fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) =
+        is_type_kind_of_monotonic T
+      | is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
+        is_type_kind_of_monotonic T
+      | is_shallow_datatype_finitizable T =
+        case triple_lookup (type_match thy) finitizes T of
+          SOME (SOME b) => b
+        | _ => is_type_kind_of_monotonic T
     fun is_datatype_deep T =
       not standard orelse T = nat_T orelse is_word_type T orelse
       exists (curry (op =) T o domain_type o type_of) sel_names
@@ -371,7 +386,7 @@
     val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
     val _ =
       if verbose andalso not unique_scope then
-        case filter_out is_type_always_monotonic mono_Ts of
+        case filter_out is_type_fundamentally_monotonic mono_Ts of
           [] => ()
         | interesting_mono_Ts =>
           print_v (K (monotonicity_message interesting_mono_Ts
@@ -382,7 +397,7 @@
       all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
     val finitizable_dataTs =
       shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
-                     |> filter is_type_finitizable
+                     |> filter is_shallow_datatype_finitizable
     val _ =
       if verbose andalso not (null finitizable_dataTs) then
         print_v (K (monotonicity_message finitizable_dataTs
@@ -649,6 +664,8 @@
                          ? cons ("user_axioms", "\"true\"")
                       |> not (none_true wfs)
                          ? cons ("wf", "\"smart\" or \"false\"")
+                      |> not sound_finitizes
+                         ? cons ("finitize", "\"smart\" or \"false\"")
                       |> not codatatypes_ok
                          ? cons ("bisim_depth", "a nonnegative value")
                  val ss =
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -65,8 +65,8 @@
   val strip_any_connective : term -> term list * term
   val conjuncts_of : term -> term list
   val disjuncts_of : term -> term list
-  val unarize_and_unbox_type : typ -> typ
-  val unarize_unbox_and_uniterize_type : typ -> typ
+  val unarize_unbox_etc_type : typ -> typ
+  val uniterize_unarize_unbox_etc_type : typ -> typ
   val string_for_type : Proof.context -> typ -> string
   val prefix_name : string -> string -> string
   val shortest_name : string -> string
@@ -148,11 +148,13 @@
     theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
   val construct_value :
     theory -> (typ option * bool) list -> styp -> term list -> term
+  val coerce_term : hol_context -> typ list -> typ -> typ -> term -> term
   val card_of_type : (typ * int) list -> typ -> int
   val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
   val bounded_exact_card_of_type :
     hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
   val is_finite_type : hol_context -> typ -> bool
+  val is_small_finite_type : hol_context -> typ -> bool
   val special_bounds : term list -> (indexname * typ) list
   val abs_var : indexname * typ -> term -> term
   val is_funky_typedef : theory -> typ -> bool
@@ -401,22 +403,24 @@
   | unarize_type @{typ "signed_bit word"} = int_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 (Type (s, Ts as _ :: _)) =
-    Type (s, map unarize_and_unbox_type Ts)
-  | unarize_and_unbox_type T = T
+fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) =
+    unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
+  | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
+    unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
+  | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
+    Type (@{type_name "*"}, map unarize_unbox_etc_type Ts)
+  | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T
+  | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T
+  | unarize_unbox_etc_type (Type (s, Ts as _ :: _)) =
+    Type (s, map unarize_unbox_etc_type Ts)
+  | unarize_unbox_etc_type T = T
 fun uniterize_type (Type (s, Ts as _ :: _)) = Type (s, map uniterize_type Ts)
   | uniterize_type @{typ bisim_iterator} = nat_T
   | uniterize_type T = T
-val unarize_unbox_and_uniterize_type = uniterize_type o unarize_and_unbox_type
+val uniterize_unarize_unbox_etc_type = uniterize_type o unarize_unbox_etc_type
 
 (* Proof.context -> typ -> string *)
-fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
+fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_unbox_etc_type
 
 (* string -> string -> string *)
 val prefix_name = Long_Name.qualify o Long_Name.base_name
@@ -439,9 +443,10 @@
   #> map_types shorten_names_in_type
 
 (* theory -> typ * typ -> bool *)
-fun type_match thy (T1, T2) =
+fun strict_type_match thy (T1, T2) =
   (Sign.typ_match thy (T2, T1) Vartab.empty; true)
   handle Type.TYPE_MATCH => false
+fun type_match thy = strict_type_match thy o pairself unarize_unbox_etc_type
 (* theory -> styp * styp -> bool *)
 fun const_match thy ((s1, T1), (s2, T2)) =
   s1 = s2 andalso type_match thy (T1, T2)
@@ -454,14 +459,14 @@
 (* typ -> bool *)
 fun is_TFree (TFree _) = true
   | is_TFree _ = false
-fun is_higher_order_type (Type ("fun", _)) = true
+fun is_higher_order_type (Type (@{type_name fun}, _)) = true
   | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
   | is_higher_order_type _ = false
-fun is_fun_type (Type ("fun", _)) = true
+fun is_fun_type (Type (@{type_name fun}, _)) = true
   | is_fun_type _ = false
-fun is_set_type (Type ("fun", [_, @{typ bool}])) = true
+fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
   | is_set_type _ = false
-fun is_pair_type (Type ("*", _)) = true
+fun is_pair_type (Type (@{type_name "*"}, _)) = true
   | is_pair_type _ = false
 fun is_lfp_iterator_type (Type (s, _)) = String.isPrefix lfp_iterator_prefix s
   | is_lfp_iterator_type _ = false
@@ -494,19 +499,20 @@
 
 (* int -> typ -> typ list * typ *)
 fun strip_n_binders 0 T = ([], T)
-  | strip_n_binders n (Type ("fun", [T1, T2])) =
+  | strip_n_binders n (Type (@{type_name fun}, [T1, T2])) =
     strip_n_binders (n - 1) T2 |>> cons T1
   | strip_n_binders n (Type (@{type_name fun_box}, Ts)) =
-    strip_n_binders n (Type ("fun", Ts))
+    strip_n_binders n (Type (@{type_name fun}, Ts))
   | strip_n_binders _ T = raise TYPE ("Nitpick_HOL.strip_n_binders", [T], [])
 (* typ -> typ *)
 val nth_range_type = snd oo strip_n_binders
 
 (* typ -> int *)
-fun num_factors_in_type (Type ("*", [T1, T2])) =
+fun num_factors_in_type (Type (@{type_name "*"}, [T1, T2])) =
     fold (Integer.add o num_factors_in_type) [T1, T2] 0
   | num_factors_in_type _ = 1
-fun num_binder_types (Type ("fun", [_, T2])) = 1 + num_binder_types T2
+fun num_binder_types (Type (@{type_name fun}, [_, T2])) =
+    1 + num_binder_types T2
   | num_binder_types _ = 0
 (* typ -> typ list *)
 val curried_binder_types = maps HOLogic.flatten_tupleT o binder_types
@@ -515,7 +521,7 @@
 
 (* typ -> term list -> term *)
 fun mk_flat_tuple _ [t] = t
-  | mk_flat_tuple (Type ("*", [T1, T2])) (t :: ts) =
+  | mk_flat_tuple (Type (@{type_name "*"}, [T1, T2])) (t :: ts) =
     HOLogic.pair_const T1 T2 $ t $ (mk_flat_tuple T2 ts)
   | mk_flat_tuple T ts = raise TYPE ("Nitpick_HOL.mk_flat_tuple", [T], ts)
 (* int -> term -> term list *)
@@ -595,7 +601,7 @@
     val (co_s, co_Ts) = dest_Type co_T
     val _ =
       if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
-         co_s <> "fun" andalso
+         co_s <> @{type_name fun} andalso
          not (is_basic_datatype thy [(NONE, true)] co_s) then
         ()
       else
@@ -669,7 +675,7 @@
   find_index (curry (op =) s o fst)
              (Record.get_extT_fields thy T1 ||> single |> op @)
 (* theory -> styp -> bool *)
-fun is_record_get thy (s, Type ("fun", [T1, _])) =
+fun is_record_get thy (s, Type (@{type_name fun}, [T1, _])) =
     exists (curry (op =) s o fst) (all_record_fields thy T1)
   | is_record_get _ _ = false
 fun is_record_update thy (s, T) =
@@ -677,30 +683,33 @@
   exists (curry (op =) (unsuffix Record.updateN s) o fst)
          (all_record_fields thy (body_type T))
   handle TYPE _ => false
-fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
+fun is_abs_fun thy (s, Type (@{type_name fun}, [_, Type (s', _)])) =
     (case typedef_info thy s' of
        SOME {Abs_name, ...} => s = Abs_name
      | NONE => false)
   | is_abs_fun _ _ = false
-fun is_rep_fun thy (s, Type ("fun", [Type (s', _), _])) =
+fun is_rep_fun thy (s, Type (@{type_name fun}, [Type (s', _), _])) =
     (case typedef_info thy s' of
        SOME {Rep_name, ...} => s = Rep_name
      | NONE => false)
   | is_rep_fun _ _ = false
 (* Proof.context -> styp -> bool *)
-fun is_quot_abs_fun ctxt (x as (_, Type ("fun", [_, Type (s', _)]))) =
+fun is_quot_abs_fun ctxt
+                    (x as (_, Type (@{type_name fun}, [_, Type (s', _)]))) =
     (try (Quotient_Term.absrep_const_chk Quotient_Term.AbsF ctxt) s'
      = SOME (Const x))
   | is_quot_abs_fun _ _ = false
-fun is_quot_rep_fun ctxt (x as (_, Type ("fun", [Type (s', _), _]))) =
+fun is_quot_rep_fun ctxt
+                    (x as (_, Type (@{type_name fun}, [Type (s', _), _]))) =
     (try (Quotient_Term.absrep_const_chk Quotient_Term.RepF ctxt) s'
      = SOME (Const x))
   | is_quot_rep_fun _ _ = false
 
 (* theory -> styp -> styp *)
-fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
+fun mate_of_rep_fun thy (x as (_, Type (@{type_name fun},
+                                        [T1 as Type (s', _), T2]))) =
     (case typedef_info thy s' of
-       SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
+       SOME {Abs_name, ...} => (Abs_name, Type (@{type_name fun}, [T2, T1]))
      | NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
   | mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
 (* theory -> typ -> typ *)
@@ -729,10 +738,10 @@
   end
   handle TYPE ("dest_Type", _, _) => false
 fun is_constr_like thy (s, T) =
-  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 (_, T)) = (s, unarize_and_unbox_type T) in
+  member (op =) [@{const_name FinFun}, @{const_name FunBox},
+                 @{const_name PairBox}, @{const_name Quot},
+                 @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
+  let val (x as (_, T)) = (s, unarize_unbox_etc_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
     is_coconstr thy x
@@ -749,8 +758,8 @@
 (* string -> bool *)
 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
 val is_sel_like_and_no_discr =
-  String.isPrefix sel_prefix
-  orf (member (op =) [@{const_name fst}, @{const_name snd}])
+  String.isPrefix sel_prefix orf
+  (member (op =) [@{const_name fst}, @{const_name snd}])
 
 (* boxability -> boxability *)
 fun in_fun_lhs_for InConstr = InSel
@@ -763,10 +772,10 @@
 (* hol_context -> boxability -> typ -> bool *)
 fun is_boxing_worth_it (hol_ctxt : hol_context) boxy T =
   case T of
-    Type ("fun", _) =>
+    Type (@{type_name fun}, _) =>
     (boxy = InPair orelse boxy = InFunLHS) andalso
     not (is_boolean_type (body_type T))
-  | Type ("*", Ts) =>
+  | Type (@{type_name "*"}, Ts) =>
     boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
     ((boxy = InExpr orelse boxy = InFunLHS) andalso
      exists (is_boxing_worth_it hol_ctxt InPair)
@@ -780,7 +789,7 @@
 (* hol_context -> boxability -> typ -> typ *)
 and box_type hol_ctxt boxy T =
   case T of
-    Type (z as ("fun", [T1, T2])) =>
+    Type (z as (@{type_name fun}, [T1, T2])) =>
     if boxy <> InConstr andalso boxy <> InSel andalso
        should_box_type hol_ctxt boxy z then
       Type (@{type_name fun_box},
@@ -788,12 +797,13 @@
     else
       box_type hol_ctxt (in_fun_lhs_for boxy) T1
       --> box_type hol_ctxt (in_fun_rhs_for boxy) T2
-  | Type (z as ("*", Ts)) =>
+  | Type (z as (@{type_name "*"}, Ts)) =>
     if boxy <> InConstr andalso boxy <> InSel
        andalso should_box_type hol_ctxt boxy z then
       Type (@{type_name pair_box}, map (box_type hol_ctxt InSel) Ts)
     else
-      Type ("*", map (box_type hol_ctxt
+      Type (@{type_name "*"},
+            map (box_type hol_ctxt
                           (if boxy = InConstr orelse boxy = InSel then boxy
                            else InPair)) Ts)
   | _ => T
@@ -979,7 +989,7 @@
     else
       let
         (* int -> typ -> int * term *)
-        fun aux m (Type ("*", [T1, T2])) =
+        fun aux m (Type (@{type_name "*"}, [T1, T2])) =
             let
               val (m, t1) = aux m T1
               val (m, t2) = aux m T2
@@ -1018,10 +1028,85 @@
       | _ => list_comb (Const x, args)
     end
 
+(* hol_context -> typ -> term -> term *)
+fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
+  (case head_of t of
+     Const x => if is_constr_like thy x then t else raise SAME ()
+   | _ => raise SAME ())
+  handle SAME () =>
+         let
+           val x' as (_, T') =
+             if is_pair_type T then
+               let val (T1, T2) = HOLogic.dest_prodT T in
+                 (@{const_name Pair}, T1 --> T2 --> T)
+               end
+             else
+               datatype_constrs hol_ctxt T |> hd
+           val arg_Ts = binder_types T'
+         in
+           list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
+                                     (index_seq 0 (length arg_Ts)) arg_Ts)
+         end
+
+(* (term -> term) -> int -> term -> term *)
+fun coerce_bound_no f j t =
+  case t of
+    t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
+  | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
+  | Bound j' => if j' = j then f t else t
+  | _ => t
+(* hol_context -> typ -> typ -> term -> term *)
+fun coerce_bound_0_in_term hol_ctxt new_T old_T =
+  old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
+(* hol_context -> typ list -> typ -> typ -> term -> term *)
+and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
+  if old_T = new_T then
+    t
+  else
+    case (new_T, old_T) of
+      (Type (new_s, new_Ts as [new_T1, new_T2]),
+       Type (@{type_name fun}, [old_T1, old_T2])) =>
+      (case eta_expand Ts t 1 of
+         Abs (s, _, t') =>
+         Abs (s, new_T1,
+              t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
+                 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
+         |> Envir.eta_contract
+         |> new_s <> @{type_name fun}
+            ? construct_value thy stds
+                  (if new_s = @{type_name fin_fun} then @{const_name FinFun}
+                   else @{const_name FunBox},
+                   Type (@{type_name fun}, new_Ts) --> new_T)
+              o single
+       | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']))
+    | (Type (new_s, new_Ts as [new_T1, new_T2]),
+       Type (old_s, old_Ts as [old_T1, old_T2])) =>
+      if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
+         old_s = @{type_name pair_box} orelse old_s = @{type_name "*"} then
+        case constr_expand hol_ctxt old_T t of
+          Const (old_s, _) $ t1 =>
+          if new_s = @{type_name fun} then
+            coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1
+          else
+            construct_value thy stds
+                (old_s, Type (@{type_name fun}, new_Ts) --> new_T)
+                [coerce_term hol_ctxt Ts (Type (@{type_name fun}, new_Ts))
+                             (Type (@{type_name fun}, old_Ts)) t1]
+        | Const _ $ t1 $ t2 =>
+          construct_value thy stds
+              (if new_s = @{type_name "*"} then @{const_name Pair}
+               else @{const_name PairBox}, new_Ts ---> new_T)
+              (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
+                    [t1, t2])
+        | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])
+      else
+        raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
+    | _ => raise TYPE ("Nitpick_HOL.coerce_term", [new_T, old_T], [t])
+
 (* (typ * int) list -> typ -> int *)
-fun card_of_type assigns (Type ("fun", [T1, T2])) =
+fun card_of_type assigns (Type (@{type_name fun}, [T1, T2])) =
     reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
-  | card_of_type assigns (Type ("*", [T1, T2])) =
+  | card_of_type assigns (Type (@{type_name "*"}, [T1, T2])) =
     card_of_type assigns T1 * card_of_type assigns T2
   | card_of_type _ (Type (@{type_name itself}, _)) = 1
   | card_of_type _ @{typ prop} = 2
@@ -1033,7 +1118,8 @@
     | NONE => if T = @{typ bisim_iterator} then 0
               else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
 (* int -> (typ * int) list -> typ -> int *)
-fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) =
+fun bounded_card_of_type max default_card assigns
+                         (Type (@{type_name fun}, [T1, T2])) =
     let
       val k1 = bounded_card_of_type max default_card assigns T1
       val k2 = bounded_card_of_type max default_card assigns T2
@@ -1041,7 +1127,8 @@
       if k1 = max orelse k2 = max then max
       else Int.min (max, reasonable_power k2 k1)
     end
-  | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) =
+  | bounded_card_of_type max default_card assigns
+                         (Type (@{type_name "*"}, [T1, T2])) =
     let
       val k1 = bounded_card_of_type max default_card assigns T1
       val k2 = bounded_card_of_type max default_card assigns T2
@@ -1064,7 +1151,7 @@
        else if member (op =) finitizable_dataTs T then
          raise SAME ()
        else case T of
-         Type ("fun", [T1, T2]) =>
+         Type (@{type_name fun}, [T1, T2]) =>
          let
            val k1 = aux avoid T1
            val k2 = aux avoid T2
@@ -1073,7 +1160,7 @@
            else if k1 >= max orelse k2 >= max then max
            else Int.min (max, reasonable_power k2 k1)
          end
-       | Type ("*", [T1, T2]) =>
+       | Type (@{type_name "*"}, [T1, T2]) =>
          let
            val k1 = aux avoid T1
            val k2 = aux avoid T2
@@ -1104,9 +1191,16 @@
              AList.lookup (op =) assigns T |> the_default default_card
   in Int.min (max, aux [] T) end
 
+val small_type_max_card = 5
+
 (* hol_context -> typ -> bool *)
 fun is_finite_type hol_ctxt T =
-  bounded_exact_card_of_type hol_ctxt [] 1 2 [] T <> 0
+  bounded_exact_card_of_type hol_ctxt [] 1 2 [] T > 0
+(* hol_context -> typ -> bool *)
+fun is_small_finite_type hol_ctxt T =
+  let val n = bounded_exact_card_of_type hol_ctxt [] 1 2 [] T in
+    n > 0 andalso n <= small_type_max_card
+  end
 
 (* term -> bool *)
 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
@@ -1144,7 +1238,8 @@
     is_typedef_axiom thy boring t2
   | is_typedef_axiom thy boring
         (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
-         $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
+         $ Const (_, Type (@{type_name fun}, [Type (s, _), _]))
+         $ Const _ $ _)) =
     boring <> is_funky_typedef_name thy s andalso is_typedef thy s
   | is_typedef_axiom _ _ _ = false
 
@@ -1538,8 +1633,8 @@
 fun is_inductive_pred hol_ctxt =
   is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt)
 fun is_equational_fun hol_ctxt =
-  (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt
-   orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
+  (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf
+   (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
 
 (* term * term -> term *)
 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
@@ -1586,7 +1681,7 @@
     fun do_term depth Ts t =
       case t of
         (t0 as Const (@{const_name Int.number_class.number_of},
-                      Type ("fun", [_, ran_T]))) $ t1 =>
+                      Type (@{type_name fun}, [_, ran_T]))) $ t1 =>
         ((if is_number_type thy ran_T then
             let
               val j = t1 |> HOLogic.dest_numeral
@@ -1612,7 +1707,7 @@
         betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
                    map (do_term depth Ts) [t1, t2])
       | Const (x as (@{const_name distinct},
-               Type ("fun", [Type (@{type_name list}, [T']), _])))
+               Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
         $ (t1 as _ $ _) =>
         (t1 |> HOLogic.dest_list |> distinctness_formula T'
          handle TERM _ => do_const depth Ts t x [t1])
@@ -1969,7 +2064,7 @@
     val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
     val set_T = tuple_T --> bool_T
     val curried_T = tuple_T --> set_T
-    val uncurried_T = Type ("*", [tuple_T, tuple_T]) --> bool_T
+    val uncurried_T = Type (@{type_name "*"}, [tuple_T, tuple_T]) --> bool_T
     val (base_rhs, step_rhs) = linear_pred_base_and_step_rhss fp_app
     val base_x as (base_s, _) = (base_prefix ^ s, outer_Ts ---> set_T)
     val base_eq = HOLogic.mk_eq (list_comb (Const base_x, outer_vars), base_rhs)
@@ -2092,8 +2187,8 @@
   let
     fun aux T accum =
       case T of
-        Type ("fun", Ts) => fold aux Ts accum
-      | Type ("*", Ts) => fold aux Ts accum
+        Type (@{type_name fun}, Ts) => fold aux Ts accum
+      | Type (@{type_name "*"}, 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)
@@ -2161,7 +2256,7 @@
 (* int list -> int list -> typ -> typ *)
 fun format_type default_format format T =
   let
-    val T = unarize_unbox_and_uniterize_type T
+    val T = uniterize_unarize_unbox_etc_type T
     val format = format |> filter (curry (op <) 0)
   in
     if forall (curry (op =) 1) format then
@@ -2200,7 +2295,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, unarize_and_unbox_type T)
+             AList.find (op =) (!special_funs) (s, unarize_unbox_etc_type T)
              |> the_single
            val max_j = List.last js
            val Ts = List.take (binder_types T', max_j + 1)
@@ -2294,7 +2389,7 @@
          let val t = Const (original_name s, T) in
            (t, format_term_type thy def_table formats t)
          end)
-      |>> map_types unarize_unbox_and_uniterize_type
+      |>> map_types uniterize_unarize_unbox_etc_type
       |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
   in do_const end
 
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -39,6 +39,7 @@
    ("bits", ["1,2,3,4,6,8,10,12"]),
    ("bisim_depth", ["7"]),
    ("box", ["smart"]),
+   ("finitize", ["smart"]),
    ("mono", ["smart"]),
    ("std", ["true"]),
    ("wf", ["smart"]),
@@ -78,6 +79,7 @@
 
 val negated_params =
   [("dont_box", "box"),
+   ("dont_finitize", "finitize"),
    ("non_mono", "mono"),
    ("non_std", "std"),
    ("non_wf", "wf"),
@@ -111,8 +113,8 @@
   AList.defined (op =) negated_params s orelse
   s = "max" orelse s = "eval" orelse s = "expect" orelse
   exists (fn p => String.isPrefix (p ^ " ") s)
-         ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "std",
-          "non_std", "wf", "non_wf", "format"]
+         ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
+          "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
 
 (* string * 'a -> unit *)
 fun check_raw_param (s, _) =
@@ -297,14 +299,8 @@
     val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
     val bitss = lookup_int_seq "bits" 1
     val bisim_depths = lookup_int_seq "bisim_depth" ~1
-    val boxes =
-      lookup_bool_option_assigns read_type_polymorphic "box" @
-      map_filter (fn (SOME T, _) =>
-                     if is_fun_type T orelse is_pair_type T then
-                       SOME (SOME T, SOME true)
-                     else
-                       NONE
-                   | (NONE, _) => NONE) cards_assigns
+    val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
+    val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
     val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
     val stds = lookup_bool_assigns read_type_polymorphic "std"
     val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
@@ -349,8 +345,8 @@
   in
     {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
      iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
-     boxes = boxes, monos = monos, stds = stds, wfs = wfs,
-     sat_solver = sat_solver, blocking = blocking, falsify = falsify,
+     boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,
+     wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
      debug = debug, verbose = verbose, overlord = overlord,
      user_axioms = user_axioms, assms = assms,
      merge_type_vars = merge_type_vars, binary_ints = binary_ints,
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -301,8 +301,8 @@
 
 (* Proof.context -> bool -> dtype_spec list -> nut -> KK.bound *)
 fun bound_for_sel_rel ctxt debug dtypes
-        (FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2),
-                  nick)) =
+        (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
+                  R as Func (Atom (_, j0), R2), nick)) =
     let
       val {delta, epsilon, exclusive, explicit_max, ...} =
         constr_spec dtypes (original_name nick, T1)
@@ -1208,7 +1208,7 @@
                            (rel_expr_from_rel_expr kk min_R R2 r2))
           end
       | Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
-      | Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) =>
+      | Cst (Iden, T as Type (@{type_name fun}, [T1, _]), R as Func (R1, _)) =>
         to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
       | Cst (Num j, T, R) =>
         if is_word_type T then
@@ -1229,36 +1229,36 @@
       | Cst (Suc, @{typ "nat => nat"}, Func (Atom x, _)) =>
         kk_intersect (KK.Rel suc_rel) (kk_product KK.Univ (KK.AtomSeq x))
       | Cst (Suc, _, Func (Atom _, _)) => KK.Rel suc_rel
-      | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_add_rel
-      | Cst (Add, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_add_rel
-      | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+      | Cst (Add, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_add_rel
+      | Cst (Add, Type (_, [@{typ int}, _]), _) => KK.Rel int_add_rel
+      | Cst (Add, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
         to_bit_word_binary_op T R NONE (SOME (curry KK.Add))
-      | Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+      | Cst (Add, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
         to_bit_word_binary_op T R
             (SOME (fn i1 => fn i2 => fn i3 =>
                  kk_implies (KK.LE (KK.Num 0, KK.BitXor (i1, i2)))
                             (KK.LE (KK.Num 0, KK.BitXor (i2, i3)))))
             (SOME (curry KK.Add))
-      | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) =>
+      | Cst (Subtract, Type (_, [@{typ nat}, _]), _) =>
         KK.Rel nat_subtract_rel
-      | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) =>
+      | Cst (Subtract, Type (_, [@{typ int}, _]), _) =>
         KK.Rel int_subtract_rel
-      | Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+      | Cst (Subtract, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
         to_bit_word_binary_op T R NONE
             (SOME (fn i1 => fn i2 =>
                       KK.IntIf (KK.LE (i1, i2), KK.Num 0, KK.Sub (i1, i2))))
-      | Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+      | Cst (Subtract, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
         to_bit_word_binary_op T R
             (SOME (fn i1 => fn i2 => fn i3 =>
                  kk_implies (KK.LT (KK.BitXor (i1, i2), KK.Num 0))
                             (KK.LT (KK.BitXor (i2, i3), KK.Num 0))))
             (SOME (curry KK.Sub))
-      | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) =>
+      | Cst (Multiply, Type (_, [@{typ nat}, _]), _) =>
         KK.Rel nat_multiply_rel
-      | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) =>
+      | Cst (Multiply, Type (_, [@{typ int}, _]), _) =>
         KK.Rel int_multiply_rel
       | Cst (Multiply,
-             T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) =>
+             T as Type (_, [Type (@{type_name word}, [bit_T]), _]), R) =>
         to_bit_word_binary_op T R
             (SOME (fn i1 => fn i2 => fn i3 =>
                 kk_or (KK.IntEq (i2, KK.Num 0))
@@ -1267,14 +1267,14 @@
                           ? kk_and (KK.LE (KK.Num 0,
                                            foldl1 KK.BitAnd [i1, i2, i3])))))
             (SOME (curry KK.Mult))
-      | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => KK.Rel nat_divide_rel
-      | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => KK.Rel int_divide_rel
-      | Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+      | Cst (Divide, Type (_, [@{typ nat}, _]), _) => KK.Rel nat_divide_rel
+      | Cst (Divide, Type (_, [@{typ int}, _]), _) => KK.Rel int_divide_rel
+      | Cst (Divide, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
         to_bit_word_binary_op T R NONE
             (SOME (fn i1 => fn i2 =>
                       KK.IntIf (KK.IntEq (i2, KK.Num 0),
                                 KK.Num 0, KK.Div (i1, i2))))
-      | Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+      | Cst (Divide, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
         to_bit_word_binary_op T R
             (SOME (fn i1 => fn i2 => fn i3 =>
                       KK.LE (KK.Num 0, foldl1 KK.BitAnd [i1, i2, i3])))
@@ -1293,9 +1293,9 @@
       | Cst (Fracs, _, Func (Struct _, _)) =>
         kk_project_seq (KK.Rel norm_frac_rel) 2 2
       | Cst (NormFrac, _, _) => KK.Rel norm_frac_rel
-      | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
+      | Cst (NatToInt, Type (_, [@{typ nat}, _]), Func (Atom _, Atom _)) =>
         KK.Iden
-      | Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
+      | Cst (NatToInt, Type (_, [@{typ nat}, _]),
              Func (Atom (_, nat_j0), Opt (Atom (int_k, int_j0)))) =>
         if nat_j0 = int_j0 then
           kk_intersect KK.Iden
@@ -1303,9 +1303,9 @@
                           KK.Univ)
         else
           raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
-      | Cst (NatToInt, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+      | Cst (NatToInt, T as Type (_, [@{typ "unsigned_bit word"}, _]), R) =>
         to_bit_word_unary_op T R I
-      | Cst (IntToNat, Type ("fun", [@{typ int}, _]),
+      | Cst (IntToNat, Type (_, [@{typ int}, _]),
              Func (Atom (int_k, int_j0), nat_R)) =>
         let
           val abs_card = max_int_for_card int_k + 1
@@ -1321,7 +1321,7 @@
           else
             raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
         end
-      | Cst (IntToNat, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+      | Cst (IntToNat, T as Type (_, [@{typ "signed_bit word"}, _]), R) =>
         to_bit_word_unary_op T R
             (fn i => KK.IntIf (KK.LE (i, KK.Num 0), KK.Num 0, i))
       | Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -110,48 +110,53 @@
   the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
 
 (* term -> term *)
-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, _])]))
-                            $ t1 $ t2) =
-    let val Ts = map unarize_unbox_and_uniterize_type [T1, T2] in
-      Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
-      $ unarize_and_unbox_term t1 $ unarize_and_unbox_term t2
+fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
+    unarize_unbox_etc_term t1
+  | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
+    unarize_unbox_etc_term t1
+  | unarize_unbox_etc_term
+        (Const (@{const_name PairBox},
+                Type (@{type_name fun}, [T1, Type (@{type_name fun}, [T2, _])]))
+         $ t1 $ t2) =
+    let val Ts = map uniterize_unarize_unbox_etc_type [T1, T2] in
+      Const (@{const_name Pair}, Ts ---> Type (@{type_name "*"}, Ts))
+      $ unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
     end
-  | unarize_and_unbox_term (Const (s, T)) =
-    Const (s, unarize_unbox_and_uniterize_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_unbox_and_uniterize_type T)
-  | unarize_and_unbox_term (Var (x, T)) =
-    Var (x, unarize_unbox_and_uniterize_type T)
-  | unarize_and_unbox_term (Bound j) = Bound j
-  | unarize_and_unbox_term (Abs (s, T, t')) =
-    Abs (s, unarize_unbox_and_uniterize_type T, unarize_and_unbox_term t')
+  | unarize_unbox_etc_term (Const (s, T)) =
+    Const (s, uniterize_unarize_unbox_etc_type T)
+  | unarize_unbox_etc_term (t1 $ t2) =
+    unarize_unbox_etc_term t1 $ unarize_unbox_etc_term t2
+  | unarize_unbox_etc_term (Free (s, T)) =
+    Free (s, uniterize_unarize_unbox_etc_type T)
+  | unarize_unbox_etc_term (Var (x, T)) =
+    Var (x, uniterize_unarize_unbox_etc_type T)
+  | unarize_unbox_etc_term (Bound j) = Bound j
+  | unarize_unbox_etc_term (Abs (s, T, t')) =
+    Abs (s, uniterize_unarize_unbox_etc_type T, unarize_unbox_etc_term t')
 
 (* typ -> typ -> (typ * typ) * (typ * typ) *)
-fun factor_out_types (T1 as Type ("*", [T11, T12]))
-                     (T2 as Type ("*", [T21, T22])) =
+fun factor_out_types (T1 as Type (@{type_name "*"}, [T11, T12]))
+                     (T2 as Type (@{type_name "*"}, [T21, T22])) =
     let val (n1, n2) = pairself num_factors_in_type (T11, T21) in
       if n1 = n2 then
         let
           val ((T11', opt_T12'), (T21', opt_T22')) = factor_out_types T12 T22
         in
-          ((Type ("*", [T11, T11']), opt_T12'),
-           (Type ("*", [T21, T21']), opt_T22'))
+          ((Type (@{type_name "*"}, [T11, T11']), opt_T12'),
+           (Type (@{type_name "*"}, [T21, T21']), opt_T22'))
         end
       else if n1 < n2 then
         case factor_out_types T1 T21 of
           (p1, (T21', NONE)) => (p1, (T21', SOME T22))
         | (p1, (T21', SOME T22')) =>
-          (p1, (T21', SOME (Type ("*", [T22', T22]))))
+          (p1, (T21', SOME (Type (@{type_name "*"}, [T22', T22]))))
       else
         swap (factor_out_types T2 T1)
     end
-  | factor_out_types (Type ("*", [T11, T12])) T2 = ((T11, SOME T12), (T2, NONE))
-  | factor_out_types T1 (Type ("*", [T21, T22])) = ((T1, NONE), (T21, SOME T22))
+  | factor_out_types (Type (@{type_name "*"}, [T11, T12])) T2 =
+    ((T11, SOME T12), (T2, NONE))
+  | factor_out_types T1 (Type (@{type_name "*"}, [T21, T22])) =
+    ((T1, NONE), (T21, SOME T22))
   | factor_out_types T1 T2 = ((T1, NONE), (T2, NONE))
 
 (* bool -> typ -> typ -> (term * term) list -> term *)
@@ -188,10 +193,11 @@
     val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
   in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
 (* typ -> term -> term -> term *)
-fun pair_up (Type ("*", [T1', T2']))
+fun pair_up (Type (@{type_name "*"}, [T1', T2']))
             (t1 as Const (@{const_name Pair},
-                          Type ("fun", [_, Type ("fun", [_, T1])])) $ t11 $ t12)
-            t2 =
+                          Type (@{type_name fun},
+                                [_, Type (@{type_name fun}, [_, T1])]))
+             $ t11 $ t12) t2 =
     if T1 = T1' then HOLogic.mk_prod (t1, t2)
     else HOLogic.mk_prod (t11, pair_up T2' t12 t2)
   | pair_up _ t1 t2 = HOLogic.mk_prod (t1, t2)
@@ -199,7 +205,7 @@
 fun multi_pair_up T1 t1 (ts2, ts3) = map2 (pair o pair_up T1 t1) ts2 ts3
 
 (* typ -> typ -> typ -> term -> term *)
-fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t =
+fun typecast_fun (Type (@{type_name fun}, [T1', T2'])) T1 T2 t =
     let
       (* typ -> typ -> typ -> typ -> term -> term *)
       fun do_curry T1 T1a T1b T2 t =
@@ -238,9 +244,11 @@
           t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
         | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])
       (* typ -> typ -> term -> term *)
-      and do_term (Type ("fun", [T1', T2'])) (Type ("fun", [T1, T2])) t =
+      and do_term (Type (@{type_name fun}, [T1', T2']))
+                  (Type (@{type_name fun}, [T1, T2])) t =
           do_fun T1' T2' T1 T2 t
-        | do_term (T' as Type ("*", Ts' as [T1', T2'])) (Type ("*", [T1, T2]))
+        | do_term (T' as Type (@{type_name "*"}, Ts' as [T1', T2']))
+                  (Type (@{type_name "*"}, [T1, T2]))
                   (Const (@{const_name Pair}, _) $ t1 $ t2) =
           Const (@{const_name Pair}, Ts' ---> T')
           $ do_term T1' T1 t1 $ do_term T2' T2 t2
@@ -257,7 +265,7 @@
   | truth_const_sort_key _ = "1"
 
 (* typ -> term list -> term *)
-fun mk_tuple (Type ("*", [T1, T2])) ts =
+fun mk_tuple (Type (@{type_name "*"}, [T1, T2])) ts =
     HOLogic.mk_prod (mk_tuple T1 ts,
         mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
   | mk_tuple _ (t :: _) = t
@@ -307,8 +315,8 @@
         else
           aux tps
       end
-    (* typ -> typ -> typ -> (term * term) list -> term *)
-    fun make_map T1 T2 T2' =
+    (* bool -> typ -> typ -> typ -> (term * term) list -> term *)
+    fun make_map maybe_opt T1 T2 T2' =
       let
         val update_const = Const (@{const_name fun_upd},
                                   (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
@@ -319,7 +327,7 @@
                Const (@{const_name None}, _) => aux' ps
              | _ => update_const $ aux' ps $ t1 $ t2)
         fun aux ps =
-          if not (is_complete_type datatypes false T1) then
+          if maybe_opt andalso not (is_complete_type datatypes false T1) then
             update_const $ aux' ps $ Const (unrep, T1)
             $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
           else
@@ -328,7 +336,7 @@
     (* typ list -> term -> term *)
     fun polish_funs Ts t =
       (case fastype_of1 (Ts, t) of
-         Type ("fun", [T1, T2]) =>
+         Type (@{type_name fun}, [T1, T2]) =>
          if is_plain_fun t then
            case T2 of
              @{typ bool} =>
@@ -341,9 +349,9 @@
              end
            | Type (@{type_name option}, [T2']) =>
              let
-               val ts_pair = snd (dest_plain_fun t)
-                             |> pairself (map (polish_funs Ts))
-             in make_map T1 T2 T2' (rev (op ~~ ts_pair)) end
+               val (maybe_opt, ts_pair) =
+                 dest_plain_fun t ||> pairself (map (polish_funs Ts))
+             in make_map maybe_opt T1 T2 T2' (rev (op ~~ ts_pair)) end
            | _ => raise SAME ()
          else
            raise SAME ()
@@ -356,7 +364,7 @@
                else polish_funs Ts t1 $ polish_funs Ts t2
              | t1 $ t2 => polish_funs Ts t1 $ polish_funs Ts t2
              | Abs (s, T, t') => Abs (s, T, polish_funs (T :: Ts) t')
-             | Const (s, Type ("fun", [T1, T2])) =>
+             | Const (s, Type (@{type_name fun}, [T1, T2])) =>
                if s = opt_flag orelse s = non_opt_flag then
                  Abs ("x", T1, Const (unknown, T2))
                else
@@ -366,24 +374,24 @@
     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
-                 |> unarize_and_unbox_term
-                 |> typecast_fun (unarize_unbox_and_uniterize_type T')
-                                 (unarize_unbox_and_uniterize_type T1)
-                                 (unarize_unbox_and_uniterize_type T2)
+                 |> unarize_unbox_etc_term
+                 |> typecast_fun (uniterize_unarize_unbox_etc_type T')
+                                 (uniterize_unarize_unbox_etc_type T1)
+                                 (uniterize_unarize_unbox_etc_type T2)
     (* (typ * int) list -> typ -> typ -> int -> term *)
-    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j _ =
+    fun term_for_atom seen (T as Type (@{type_name fun}, [T1, T2])) T' j _ =
         let
           val k1 = card_of_type card_assigns T1
           val k2 = card_of_type card_assigns T2
         in
-          term_for_rep seen T T' (Vect (k1, Atom (k2, 0)))
+          term_for_rep true seen T T' (Vect (k1, Atom (k2, 0)))
                        [nth_combination (replicate k1 (k2, 0)) j]
           handle General.Subscript =>
                  raise ARG ("Nitpick_Model.reconstruct_term.term_for_atom",
                             signed_string_of_int j ^ " for " ^
                             string_for_rep (Vect (k1, Atom (k2, 0))))
         end
-      | term_for_atom seen (Type ("*", [T1, T2])) _ j k =
+      | term_for_atom seen (Type (@{type_name "*"}, [T1, T2])) _ j k =
         let
           val k1 = card_of_type card_assigns T1
           val k2 = k div k1
@@ -461,8 +469,9 @@
                   if length arg_Ts = 0 then
                     []
                   else
-                    map3 (fn Ts => term_for_rep seen Ts Ts) arg_Ts arg_Rs
-                         arg_jsss
+                    map3 (fn Ts =>
+                             term_for_rep (constr_s <> @{const_name FinFun})
+                                          seen Ts Ts) arg_Ts arg_Rs arg_jsss
                     |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
                     |> dest_n_tuple (length uncur_arg_Ts)
                 val t =
@@ -519,50 +528,54 @@
     and term_for_vect seen k R T1 T2 T' js =
       make_fun true T1 T2 T'
                (map (fn j => term_for_atom seen T1 T1 j k) (index_seq 0 k))
-               (map (term_for_rep seen T2 T2 R o single)
+               (map (term_for_rep true seen T2 T2 R o single)
                     (batch_list (arity_of_rep R) js))
-    (* (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
-    and term_for_rep seen T T' Unit [[]] = term_for_atom seen T T' 0 1
-      | term_for_rep seen T T' (R as Atom (k, j0)) [[j]] =
+    (* bool -> (typ * int) list -> typ -> typ -> rep -> int list list -> term *)
+    and term_for_rep _ seen T T' Unit [[]] = term_for_atom seen T T' 0 1
+      | term_for_rep _ seen T T' (R as Atom (k, j0)) [[j]] =
         if j >= j0 andalso j < j0 + k then term_for_atom seen T T' (j - j0) k
         else raise REP ("Nitpick_Model.reconstruct_term.term_for_rep", [R])
-      | term_for_rep seen (Type ("*", [T1, T2])) _ (Struct [R1, R2]) [js] =
+      | term_for_rep _ seen (Type (@{type_name "*"}, [T1, T2])) _
+                     (Struct [R1, R2]) [js] =
         let
           val arity1 = arity_of_rep R1
           val (js1, js2) = chop arity1 js
         in
           list_comb (HOLogic.pair_const T1 T2,
-                     map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2]
+                     map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
                           [[js1], [js2]])
         end
-      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Vect (k, R')) [js] =
+      | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
+                     (Vect (k, R')) [js] =
         term_for_vect seen k R' T1 T2 T' js
-      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, Formula Neut))
-                     jss =
+      | term_for_rep _ seen (Type (@{type_name fun}, [T1, T2])) T'
+                     (Func (R1, Formula Neut)) jss =
         let
           val jss1 = all_combinations_for_rep R1
-          val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
+          val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
           val ts2 =
-            map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
+            map (fn js => term_for_rep true seen T2 T2 (Atom (2, 0))
                                        [[int_from_bool (member (op =) jss js)]])
                 jss1
         in make_fun false T1 T2 T' ts1 ts2 end
-      | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
+      | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
+                     (Func (R1, R2)) jss =
         let
           val arity1 = arity_of_rep R1
           val jss1 = all_combinations_for_rep R1
-          val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
+          val ts1 = map (term_for_rep false seen T1 T1 R1 o single) jss1
           val grouped_jss2 = AList.group (op =) (map (chop arity1) jss)
-          val ts2 = map (term_for_rep seen T2 T2 R2 o the_default []
+          val ts2 = map (term_for_rep false seen T2 T2 R2 o the_default []
                          o AList.lookup (op =) grouped_jss2) jss1
-        in make_fun true T1 T2 T' ts1 ts2 end
-      | term_for_rep seen T T' (Opt R) jss =
-        if null jss then Const (unknown, T) else term_for_rep seen T T' R jss
-      | term_for_rep _ T _ R jss =
+        in make_fun maybe_opt T1 T2 T' ts1 ts2 end
+      | term_for_rep _ seen T T' (Opt R) jss =
+        if null jss then Const (unknown, T)
+        else term_for_rep true seen T T' R jss
+      | term_for_rep _ _ T _ R jss =
         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 unarize_and_unbox_term oooo term_for_rep [] end
+  in polish_funs [] o unarize_unbox_etc_term oooo term_for_rep true [] end
 
 (* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
    -> nut -> term *)
@@ -689,7 +702,7 @@
         val (oper, (t1, T'), T) =
           case name of
             FreeName (s, T, _) =>
-            let val t = Free (s, unarize_unbox_and_uniterize_type T) in
+            let val t = Free (s, uniterize_unarize_unbox_etc_type T) in
               ("=", (t, format_term_type thy def_table formats t), T)
             end
           | ConstName (s, T, _) =>
@@ -710,12 +723,17 @@
     (* dtype_spec -> Pretty.T *)
     fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
       Pretty.block (Pretty.breaks
-          [Syntax.pretty_typ ctxt (unarize_unbox_and_uniterize_type typ),
-           Pretty.str "=",
-           Pretty.enum "," "{" "}"
-               (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
-                (if fun_from_pair complete false then []
-                 else [Pretty.str unrep]))])
+          (Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
+           (case typ of
+              Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
+            | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
+            | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
+            | _ => []) @
+           [Pretty.str "=",
+            Pretty.enum "," "{" "}"
+                (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
+                 (if fun_from_pair complete false then []
+                  else [Pretty.str unrep]))]))
     (* typ -> dtype_spec list *)
     fun integer_datatype T =
       [{typ = T, card = card_of_type card_assigns T, co = false,
@@ -752,13 +770,14 @@
     val (eval_names, noneval_nonskolem_nonsel_names) =
       List.partition (String.isPrefix eval_prefix o nickname_of)
                      nonskolem_nonsel_names
-      ||> filter_out (curry (op =) @{const_name bisim_iterator_max}
+      ||> filter_out (member (op =) [@{const_name bisim},
+                                     @{const_name bisim_iterator_max}]
                       o nickname_of)
     val free_names =
       map (fn x as (s, T) =>
               case filter (curry (op =) x
                        o pairf nickname_of
-                               (unarize_unbox_and_uniterize_type o type_of))
+                               (uniterize_unarize_unbox_etc_type o type_of))
                        free_names of
                 [name] => name
               | [] => FreeName (s, T, Any)
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -11,6 +11,9 @@
 
   val formulas_monotonic :
     hol_context -> bool -> typ -> term list * term list -> bool
+  val finitize_funs :
+    hol_context -> bool -> (typ option * bool option) list -> typ
+    -> term list * term list -> term list * term list
 end;
 
 structure Nitpick_Mono : NITPICK_MONO =
@@ -42,14 +45,17 @@
   {hol_ctxt: hol_context,
    binarize: bool,
    alpha_T: typ,
+   no_harmless: bool,
    max_fresh: int Unsynchronized.ref,
-   datatype_cache: ((string * typ list) * mtyp) list Unsynchronized.ref,
-   constr_cache: (styp * mtyp) list Unsynchronized.ref}
+   datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
+   constr_mcache: (styp * mtyp) list Unsynchronized.ref}
 
-exception MTYPE of string * mtyp list
+exception MTYPE of string * mtyp list * typ list
+exception MTERM of string * mterm list
 
 (* string -> unit *)
 fun print_g (_ : string) = ()
+(* val print_g = tracing *)
 
 (* var -> string *)
 val string_for_var = signed_string_of_int
@@ -70,7 +76,7 @@
 
 (* sign_atom -> string *)
 fun string_for_sign_atom (S sn) = string_for_sign sn
-  | string_for_sign_atom (V j) = string_for_var j
+  | string_for_sign_atom (V x) = string_for_var x
 
 (* literal -> string *)
 fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
@@ -83,7 +89,7 @@
   | is_MRec _ = false
 (* mtyp -> mtyp * sign_atom * mtyp *)
 fun dest_MFun (MFun z) = z
-  | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M])
+  | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M], [])
 
 val no_prec = 100
 
@@ -157,13 +163,18 @@
   | mtype_of_mterm (MApp (m1, _)) =
     case mtype_of_mterm m1 of
       MFun (_, _, M12) => M12
-    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1])
+    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])
+
+(* mterm -> mterm * mterm list *)
+fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
+  | strip_mcomb m = (m, [])
 
-(* hol_context -> bool -> typ -> mdata *)
-fun initial_mdata hol_ctxt binarize alpha_T =
+(* hol_context -> bool -> bool -> typ -> mdata *)
+fun initial_mdata hol_ctxt binarize no_harmless 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 []} : mdata)
+    no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
+    datatype_mcache = Unsynchronized.ref [],
+    constr_mcache = Unsynchronized.ref []} : mdata)
 
 (* typ -> typ -> bool *)
 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
@@ -215,7 +226,7 @@
            else repair_mtype cache (M :: seen) M
 
 (* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *)
-fun repair_datatype_cache cache =
+fun repair_datatype_mcache cache =
   let
     (* (string * typ list) * mtyp -> unit *)
     fun repair_one (z, M) =
@@ -224,20 +235,41 @@
   in List.app repair_one (rev (!cache)) end
 
 (* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *)
-fun repair_constr_cache dtype_cache constr_cache =
+fun repair_constr_mcache dtype_cache constr_mcache =
   let
     (* styp * mtyp -> unit *)
     fun repair_one (x, M) =
-      Unsynchronized.change constr_cache
+      Unsynchronized.change constr_mcache
           (AList.update (op =) (x, repair_mtype dtype_cache [] M))
-  in List.app repair_one (!constr_cache) end
+  in List.app repair_one (!constr_mcache) end
+
+(* typ -> bool *)
+fun is_fin_fun_supported_type @{typ prop} = true
+  | is_fin_fun_supported_type @{typ bool} = true
+  | is_fin_fun_supported_type (Type (@{type_name option}, _)) = true
+  | is_fin_fun_supported_type _ = false
+(* typ -> typ -> term -> term option *)
+fun fin_fun_body _ _ (t as @{term False}) = SOME t
+  | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
+  | fin_fun_body dom_T ran_T
+                 ((t0 as Const (@{const_name If}, _))
+                  $ (t1 as Const (@{const_name "op ="}, _) $ Bound 0 $ t1')
+                  $ t2 $ t3) =
+    (if loose_bvar1 (t1', 0) then
+       NONE
+     else case fin_fun_body dom_T ran_T t3 of
+       NONE => NONE
+     | SOME t3 =>
+       SOME (t0 $ (Const (@{const_name is_unknown}, dom_T --> bool_T) $ t1')
+                $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
+  | fin_fun_body _ _ _ = NONE
 
 (* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
 fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
   let
     val M1 = fresh_mtype_for_type mdata T1
     val M2 = fresh_mtype_for_type mdata T2
-    val a = if is_boolean_type (body_type T2) andalso
+    val a = if is_fin_fun_supported_type (body_type T2) andalso
                exists_alpha_sub_mtype_fresh M1 then
               V (Unsynchronized.inc max_fresh)
             else
@@ -245,25 +277,23 @@
   in (M1, a, M2) end
 (* mdata -> typ -> mtyp *)
 and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
-                                    datatype_cache, constr_cache, ...}) =
+                                    datatype_mcache, constr_mcache, ...}) =
   let
-    (* typ -> typ -> mtyp *)
-    val do_fun = MFun oo fresh_mfun_for_fun_type mdata
     (* typ -> mtyp *)
     fun do_type T =
       if T = alpha_T then
         MAlpha
       else case T of
-        Type ("fun", [T1, T2]) => do_fun T1 T2
-      | Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2
-      | Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2))
+        Type (@{type_name fun}, [T1, T2]) =>
+        MFun (fresh_mfun_for_fun_type mdata T1 T2)
+      | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
       | Type (z as (s, _)) =>
         if could_exist_alpha_sub_mtype thy alpha_T T then
-          case AList.lookup (op =) (!datatype_cache) z of
+          case AList.lookup (op =) (!datatype_mcache) z of
             SOME M => M
           | NONE =>
             let
-              val _ = Unsynchronized.change datatype_cache (cons (z, MRec z))
+              val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z))
               val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
               val (all_Ms, constr_Ms) =
                 fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
@@ -279,15 +309,15 @@
                              end)
                          xs ([], [])
               val M = MType (s, all_Ms)
-              val _ = Unsynchronized.change datatype_cache
+              val _ = Unsynchronized.change datatype_mcache
                           (AList.update (op =) (z, M))
-              val _ = Unsynchronized.change constr_cache
+              val _ = Unsynchronized.change constr_mcache
                           (append (xs ~~ constr_Ms))
             in
-              if forall (not o is_MRec o snd) (!datatype_cache) then
-                (repair_datatype_cache datatype_cache;
-                 repair_constr_cache (!datatype_cache) constr_cache;
-                 AList.lookup (op =) (!datatype_cache) z |> the)
+              if forall (not o is_MRec o snd) (!datatype_mcache) then
+                (repair_datatype_mcache datatype_mcache;
+                 repair_constr_mcache (!datatype_mcache) constr_mcache;
+                 AList.lookup (op =) (!datatype_mcache) z |> the)
               else
                 M
             end
@@ -300,7 +330,7 @@
 fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
   | prodM_factors M = [M]
 (* mtyp -> mtyp list * mtyp *)
-fun curried_strip_mtype (MFun (M1, S Minus, M2)) =
+fun curried_strip_mtype (MFun (M1, _, M2)) =
     curried_strip_mtype M2 |>> append (prodM_factors M1)
   | curried_strip_mtype M = ([], M)
 (* string -> mtyp -> mtyp *)
@@ -311,36 +341,34 @@
   end
 
 (* mdata -> styp -> mtyp *)
-fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
+fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_mcache,
                                 ...}) (x as (_, T)) =
   if could_exist_alpha_sub_mtype thy alpha_T T then
-    case AList.lookup (op =) (!constr_cache) x of
+    case AList.lookup (op =) (!constr_mcache) x of
       SOME M => M
     | NONE => if T = alpha_T then
                 let val M = fresh_mtype_for_type mdata T in
-                  (Unsynchronized.change constr_cache (cons (x, M)); M)
+                  (Unsynchronized.change constr_mcache (cons (x, M)); M)
                 end
               else
                 (fresh_mtype_for_type mdata (body_type T);
-                 AList.lookup (op =) (!constr_cache) x |> the)
+                 AList.lookup (op =) (!constr_mcache) x |> the)
   else
     fresh_mtype_for_type mdata T
 fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
   x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
     |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
 
+(* literal list -> sign_atom -> sign_atom *)
+fun resolve_sign_atom lits (V x) =
+    x |> AList.lookup (op =) lits |> Option.map S |> the_default (V x)
+  | resolve_sign_atom _ a = a
 (* literal list -> mtyp -> mtyp *)
-fun instantiate_mtype lits =
+fun resolve_mtype lits =
   let
     (* mtyp -> mtyp *)
     fun aux MAlpha = MAlpha
-      | aux (MFun (M1, V x, M2)) =
-        let
-          val a = case AList.lookup (op =) lits x of
-                    SOME sn => S sn
-                  | NONE => V x
-        in MFun (aux M1, a, aux M2) end
-      | aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2)
+      | aux (MFun (M1, a, M2)) = MFun (aux M1, resolve_sign_atom lits a, aux M2)
       | aux (MPair Mp) = MPair (pairself aux Mp)
       | aux (MType (s, Ms)) = MType (s, map aux Ms)
       | aux (MRec z) = MRec z
@@ -417,11 +445,12 @@
                   accum =
     (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
      handle Library.UnequalLengths =>
-            raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]))
+            raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
   | do_mtype_comp _ _ (MType _) (MType _) accum =
     accum (* no need to compare them thanks to the cache *)
-  | do_mtype_comp _ _ M1 M2 _ =
-    raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])
+  | do_mtype_comp cmp _ M1 M2 _ =
+    raise MTYPE ("Nitpick_Mono.do_mtype_comp (" ^ string_for_comp_op cmp ^ ")",
+                 [M1, M2], [])
 
 (* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
 fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
@@ -471,20 +500,20 @@
   | do_notin_mtype_fv sn sexp (MType (_, Ms)) accum =
     accum |> fold (do_notin_mtype_fv sn sexp) Ms
   | do_notin_mtype_fv _ _ M _ =
-    raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M])
+    raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
 
 (* sign -> mtyp -> constraint_set -> constraint_set *)
 fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet
   | add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) =
-    (print_g ("*** Add " ^ string_for_mtype M ^ " is right-" ^
-              (case sn of Minus => "unique" | Plus => "total") ^ ".");
+    (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
+              (case sn of Minus => "concrete" | Plus => "complete") ^ ".");
      case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
        NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
      | SOME (lits, sexps) => CSet (lits, comps, sexps))
 
 (* mtyp -> constraint_set -> constraint_set *)
-val add_mtype_is_right_unique = add_notin_mtype_fv Minus
-val add_mtype_is_right_total = add_notin_mtype_fv Plus
+val add_mtype_is_concrete = add_notin_mtype_fv Minus
+val add_mtype_is_complete = add_notin_mtype_fv Plus
 
 val bool_from_minus = true
 
@@ -574,34 +603,35 @@
 
 type mtype_schema = mtyp * constraint_set
 type mtype_context =
-  {bounds: mtyp list,
+  {bound_Ts: typ list,
+   bound_Ms: mtyp list,
    frees: (styp * mtyp) list,
    consts: (styp * mtyp) list}
 
 type accumulator = mtype_context * constraint_set
 
-val initial_gamma = {bounds = [], frees = [], consts = []}
+val initial_gamma = {bound_Ts = [], bound_Ms = [], frees = [], consts = []}
 val unsolvable_accum = (initial_gamma, UnsolvableCSet)
 
-(* mtyp -> mtype_context -> mtype_context *)
-fun push_bound M {bounds, frees, consts} =
-  {bounds = M :: bounds, frees = frees, consts = consts}
+(* typ -> mtyp -> mtype_context -> mtype_context *)
+fun push_bound T M {bound_Ts, bound_Ms, frees, consts} =
+  {bound_Ts = T :: bound_Ts, bound_Ms = M :: bound_Ms, frees = frees,
+   consts = consts}
 (* mtype_context -> mtype_context *)
-fun pop_bound {bounds, frees, consts} =
-  {bounds = tl bounds, frees = frees, consts = consts}
-  handle List.Empty => initial_gamma
+fun pop_bound {bound_Ts, bound_Ms, frees, consts} =
+  {bound_Ts = tl bound_Ts, bound_Ms = tl bound_Ms, frees = frees,
+   consts = consts}
+  handle List.Empty => initial_gamma (* FIXME: needed? *)
 
 (* mdata -> term -> accumulator -> mterm * accumulator *)
 fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
-                                         def_table, ...},
+                                          def_table, ...},
                              alpha_T, max_fresh, ...}) =
   let
-    (* typ -> typ -> mtyp * sign_atom * mtyp *)
-    val mfun_for = fresh_mfun_for_fun_type mdata
     (* typ -> mtyp *)
     val mtype_for = fresh_mtype_for_type mdata
     (* mtyp -> mtyp *)
-    fun pos_set_mtype_for_dom M =
+    fun plus_set_mtype_for_dom M =
       MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
     (* typ -> accumulator -> mterm * accumulator *)
     fun do_all T (gamma, cset) =
@@ -610,13 +640,13 @@
         val body_M = mtype_for (body_type T)
       in
         (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
-         (gamma, cset |> add_mtype_is_right_total abs_M))
+         (gamma, cset |> add_mtype_is_complete abs_M))
       end
     fun do_equals T (gamma, cset) =
       let val M = mtype_for (domain_type T) in
         (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh),
                                  mtype_for (nth_range_type 2 T))),
-         (gamma, cset |> add_mtype_is_right_unique M))
+         (gamma, cset |> add_mtype_is_concrete M))
       end
     fun do_robust_set_operation T (gamma, cset) =
       let
@@ -633,25 +663,25 @@
         val set_T = domain_type T
         val set_M = mtype_for set_T
         (* typ -> mtyp *)
-        fun custom_mtype_for (T as Type ("fun", [T1, T2])) =
+        fun custom_mtype_for (T as Type (@{type_name fun}, [T1, T2])) =
             if T = set_T then set_M
             else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
           | custom_mtype_for T = mtype_for T
       in
-        (custom_mtype_for T, (gamma, cset |> add_mtype_is_right_unique set_M))
+        (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete set_M))
       end
     (* typ -> accumulator -> mtyp * accumulator *)
     fun do_pair_constr T accum =
       case mtype_for (nth_range_type 2 T) of
         M as MPair (a_M, b_M) =>
         (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
-      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M])
+      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M], [])
     (* int -> typ -> accumulator -> mtyp * accumulator *)
     fun do_nth_pair_sel n T =
       case mtype_for (domain_type T) of
         M as MPair (a_M, b_M) =>
         pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
-      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M])
+      | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
     (* mtyp * accumulator *)
     val mtype_unsolvable = (dummy_M, unsolvable_accum)
     (* term -> mterm * accumulator *)
@@ -661,8 +691,9 @@
     fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
       let
         val abs_M = mtype_for abs_T
-        val (bound_m, accum) = accum |>> push_bound abs_M |> do_term bound_t
-        val expected_bound_M = pos_set_mtype_for_dom abs_M
+        val (bound_m, accum) =
+          accum |>> push_bound abs_T abs_M |> do_term bound_t
+        val expected_bound_M = plus_set_mtype_for_dom abs_M
         val (body_m, accum) =
           accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
                 |> do_term body_t ||> apfst pop_bound
@@ -678,7 +709,8 @@
       end
     (* term -> accumulator -> mterm * accumulator *)
     and do_term t (_, UnsolvableCSet) = mterm_unsolvable t
-      | do_term t (accum as (gamma as {bounds, frees, consts}, cset)) =
+      | do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
+                             cset)) =
         (case t of
            Const (x as (s, T)) =>
            (case AList.lookup (op =) consts x of
@@ -714,12 +746,12 @@
                 let
                   val set_T = domain_type (range_type T)
                   val M1 = mtype_for (domain_type set_T)
-                  val M1' = pos_set_mtype_for_dom M1
+                  val M1' = plus_set_mtype_for_dom M1
                   val M2 = mtype_for set_T
                   val M3 = mtype_for set_T
                 in
                   (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
-                   (gamma, cset |> add_mtype_is_right_unique M1
+                   (gamma, cset |> add_mtype_is_concrete M1
                                 |> add_is_sub_mtype M1' M3
                                 |> add_is_sub_mtype M2 M3))
                 end
@@ -738,7 +770,7 @@
               | @{const_name finite} =>
                 if is_finite_type hol_ctxt T then
                   let val M1 = mtype_for (domain_type (domain_type T)) in
-                    (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
+                    (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
                   end
                 else
                   (print_g "*** finite"; mtype_unsolvable)
@@ -761,8 +793,8 @@
                   val b_M = mtype_for (range_type (domain_type T))
                 in
                   (MFun (MFun (a_M, S Minus, b_M), S Minus,
-                         MFun (pos_set_mtype_for_dom a_M, S Minus,
-                               pos_set_mtype_for_dom b_M)), accum)
+                         MFun (plus_set_mtype_for_dom a_M, S Minus,
+                               plus_set_mtype_for_dom b_M)), accum)
                 end
               | @{const_name Sigma} =>
                 let
@@ -784,12 +816,8 @@
               | @{const_name Tha} =>
                 let
                   val a_M = mtype_for (domain_type (domain_type T))
-                  val a_set_M = pos_set_mtype_for_dom a_M
+                  val a_set_M = plus_set_mtype_for_dom a_M
                 in (MFun (a_set_M, S Minus, a_M), accum) end
-              | @{const_name FunBox} =>
-                let val dom_M = mtype_for (domain_type T) in
-                  (MFun (dom_M, S Minus, dom_M), accum)
-                end
               | _ =>
                 if s = @{const_name minus_class.minus} andalso
                    is_set_type (domain_type T) then
@@ -800,7 +828,7 @@
                   in
                     (MFun (left_set_M, S Minus,
                            MFun (right_set_M, S Minus, left_set_M)),
-                     (gamma, cset |> add_mtype_is_right_unique right_set_M
+                     (gamma, cset |> add_mtype_is_concrete right_set_M
                                   |> add_is_sub_mtype right_set_M left_set_M))
                   end
                 else if s = @{const_name ord_class.less_eq} andalso
@@ -811,50 +839,54 @@
                         is_set_type (domain_type T) then
                   do_robust_set_operation T accum
                 else if is_sel s then
-                  if constr_name_for_sel_like s = @{const_name FunBox} then
-                    let val dom_M = mtype_for (domain_type T) in
-                      (MFun (dom_M, S Minus, dom_M), accum)
-                    end
-                  else
-                    (mtype_for_sel mdata x, accum)
+                  (mtype_for_sel mdata x, accum)
                 else if is_constr thy stds x then
                   (mtype_for_constr mdata x, accum)
-                else if is_built_in_const thy stds fast_descrs x then
+                else if is_built_in_const thy stds fast_descrs x andalso
+                        s <> @{const_name is_unknown} andalso
+                        s <> @{const_name unknown} then
+                  (* the "unknown" part is a hack *)
                   case def_of_const thy def_table x of
                     SOME t' => do_term t' accum |>> mtype_of_mterm
                   | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
                 else
                   let val M = mtype_for T in
-                    (M, ({bounds = bounds, frees = frees,
-                          consts = (x, M) :: consts}, cset))
+                    (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
+                          frees = frees, consts = (x, M) :: consts}, cset))
                   end) |>> curry MRaw t
          | Free (x as (_, T)) =>
            (case AList.lookup (op =) frees x of
               SOME M => (M, accum)
             | NONE =>
               let val M = mtype_for T in
-                (M, ({bounds = bounds, frees = (x, M) :: frees,
-                      consts = consts}, cset))
+                (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
+                      frees = (x, M) :: frees, consts = consts}, cset))
               end) |>> curry MRaw t
          | Var _ => (print_g "*** Var"; mterm_unsolvable t)
-         | Bound j => (MRaw (t, nth bounds j), accum)
-         | Abs (s, T, t' as @{const False}) =>
-           let val (M1, a, M2) = mfun_for T bool_T in
-             (MAbs (s, T, M1, a, MRaw (t', M2)), accum)
-           end
+         | Bound j => (MRaw (t, nth bound_Ms j), accum)
          | Abs (s, T, t') =>
-           ((case t' of
-               t1' $ Bound 0 =>
-               if not (loose_bvar1 (t1', 0)) then
-                 do_term (incr_boundvars ~1 t1') accum
-               else
-                 raise SAME ()
-             | _ => raise SAME ())
-            handle SAME () =>
-                   let
-                     val M = mtype_for T
-                     val (m', accum) = do_term t' (accum |>> push_bound M)
-                   in (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound) end)
+           (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
+              SOME t' =>
+              let
+                val M = mtype_for T
+                val a = V (Unsynchronized.inc max_fresh)
+                val (m', accum) = do_term t' (accum |>> push_bound T M)
+              in (MAbs (s, T, M, a, m'), accum |>> pop_bound) end
+            | NONE =>
+              ((case t' of
+                  t1' $ Bound 0 =>
+                  if not (loose_bvar1 (t1', 0)) then
+                    do_term (incr_boundvars ~1 t1') accum
+                  else
+                    raise SAME ()
+                | _ => raise SAME ())
+               handle SAME () =>
+                      let
+                        val M = mtype_for T
+                        val (m', accum) = do_term t' (accum |>> push_bound T M)
+                      in
+                        (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound)
+                      end))
          | (t0 as Const (@{const_name All}, _))
            $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
            do_bounded_quantifier t0 s' T' t10 t11 t12 accum
@@ -872,6 +904,8 @@
                (_, UnsolvableCSet) => mterm_unsolvable t
              | _ =>
                let
+                 val T11 = domain_type (fastype_of1 (bound_Ts, t1))
+                 val T2 = fastype_of1 (bound_Ts, t2)
                  val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
                  val M2 = mtype_of_mterm m2
                in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
@@ -880,18 +914,38 @@
                                       string_for_mterm ctxt m))
   in do_term end
 
-(* mdata -> styp -> term -> term -> mterm * accumulator *)
-fun consider_general_equals mdata (x as (_, T)) t1 t2 accum =
+(*
+    accum |> (case a of
+                S Minus => accum 
+              | S Plus => unsolvable_accum
+              | V x => do_literal (x, Minus) lits)
+*)
+
+(* int -> mtyp -> accumulator -> accumulator *)
+fun force_minus_funs 0 _ = I
+  | force_minus_funs n (M as MFun (M1, _, M2)) =
+    add_mtypes_equal M (MFun (M1, S Minus, M2))
+    #> force_minus_funs (n - 1) M2
+  | force_minus_funs _ M =
+    raise MTYPE ("Nitpick_Mono.force_minus_funs", [M], [])
+(* mdata -> bool -> styp -> term -> term -> mterm * accumulator *)
+fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
   let
     val (m1, accum) = consider_term mdata t1 accum
     val (m2, accum) = consider_term mdata t2 accum
     val M1 = mtype_of_mterm m1
     val M2 = mtype_of_mterm m2
+    val accum = accum ||> add_mtypes_equal M1 M2
     val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
+    val m = MApp (MApp (MRaw (Const x,
+                MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2)
   in
-    (MApp (MApp (MRaw (Const x,
-         MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2),
-     accum ||> add_mtypes_equal M1 M2)
+    (m, if def then
+          let val (head_m, arg_ms) = strip_mcomb m1 in
+            accum ||> force_minus_funs (length arg_ms) (mtype_of_mterm head_m)
+          end
+        else
+          accum)
   end
 
 (* mdata -> sign -> term -> accumulator -> mterm * accumulator *)
@@ -912,11 +966,13 @@
               val abs_M = mtype_for abs_T
               val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
               val (body_m, accum) =
-                accum ||> side_cond ? add_mtype_is_right_total abs_M
-                      |>> push_bound abs_M |> do_formula sn body_t
+                accum ||> side_cond ? add_mtype_is_complete abs_M
+                      |>> push_bound abs_T abs_M |> do_formula sn body_t
               val body_M = mtype_of_mterm body_m
             in
-              (MApp (MRaw (Const quant_x, MFun (abs_M, S Minus, body_M)),
+              (MApp (MRaw (Const quant_x,
+                           MFun (MFun (abs_M, S Minus, body_M), S Minus,
+                                 body_M)),
                      MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
                accum |>> pop_bound)
             end
@@ -924,7 +980,7 @@
           fun do_equals x t1 t2 =
             case sn of
               Plus => do_term t accum
-            | Minus => consider_general_equals mdata x t1 t2 accum
+            | Minus => consider_general_equals mdata false x t1 t2 accum
         in
           case t of
             Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
@@ -947,7 +1003,7 @@
             (case sn of
                Plus => do_quantifier x0 s1 T1 t1'
              | Minus =>
-               (* ### do elsewhere *)
+               (* FIXME: Move elsewhere *)
                do_term (@{const Not}
                         $ (HOLogic.eq_const (domain_type T0) $ t1
                            $ Abs (Name.uu, T1, @{const False}))) accum)
@@ -981,23 +1037,24 @@
   [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
 val bounteous_consts = [@{const_name bisim}]
 
-(* term -> bool *)
-fun is_harmless_axiom ({thy, stds, fast_descrs, ...} : hol_context) t =
-  Term.add_consts t []
-  |> filter_out (is_built_in_const thy stds fast_descrs)
-  |> (forall (member (op =) harmless_consts o original_name o fst)
-      orf exists (member (op =) bounteous_consts o fst))
+(* mdata -> term -> bool *)
+fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
+  | is_harmless_axiom {hol_ctxt = {thy, stds, fast_descrs, ...}, ...} t =
+    Term.add_consts t []
+    |> filter_out (is_built_in_const thy stds fast_descrs)
+    |> (forall (member (op =) harmless_consts o original_name o fst) orf
+        exists (member (op =) bounteous_consts o fst))
 
 (* mdata -> term -> accumulator -> mterm * accumulator *)
-fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) t =
-  if is_harmless_axiom hol_ctxt t then pair (MRaw (t, dummy_M))
+fun consider_nondefinitional_axiom mdata t =
+  if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
   else consider_general_formula mdata Plus t
 
 (* mdata -> term -> accumulator -> mterm * accumulator *)
-fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t =
+fun consider_definitional_axiom (mdata as {hol_ctxt = {thy, ...}, ...}) t =
   if not (is_constr_pattern_formula thy t) then
     consider_nondefinitional_axiom mdata t
-  else if is_harmless_axiom hol_ctxt t then
+  else if is_harmless_axiom mdata t then
     pair (MRaw (t, dummy_M))
   else
     let
@@ -1010,10 +1067,11 @@
         let
           val abs_M = mtype_for abs_T
           val (body_m, accum) =
-            accum |>> push_bound abs_M |> do_formula body_t
+            accum |>> push_bound abs_T abs_M |> do_formula body_t
           val body_M = mtype_of_mterm body_m
         in
-          (MApp (MRaw (quant_t, MFun (abs_M, S Minus, body_M)),
+          (MApp (MRaw (quant_t,
+                       MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M)),
                  MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
            accum |>> pop_bound)
         end
@@ -1039,16 +1097,20 @@
           case t of
             (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
             do_all t0 s1 T1 t1 accum
-          | @{const Trueprop} $ t1 => do_formula t1 accum
+          | @{const Trueprop} $ t1 =>
+            let val (m1, accum) = do_formula t1 accum in
+              (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
+                     m1), accum)
+            end
           | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
-            consider_general_equals mdata x t1 t2 accum
+            consider_general_equals mdata true x t1 t2 accum
           | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
           | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
             do_conjunction t0 t1 t2 accum
           | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
             do_all t0 s0 T1 t1 accum
           | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
-            consider_general_equals mdata x t1 t2 accum
+            consider_general_equals mdata true x t1 t2 accum
           | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
           | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
           | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
@@ -1057,8 +1119,7 @@
 
 (* Proof.context -> literal list -> term -> mtyp -> string *)
 fun string_for_mtype_of_term ctxt lits t M =
-  Syntax.string_of_term ctxt t ^ " : " ^
-  string_for_mtype (instantiate_mtype lits M)
+  Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
 
 (* theory -> literal list -> mtype_context -> unit *)
 fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
@@ -1067,31 +1128,135 @@
   |> cat_lines |> print_g
 
 (* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *)
-fun gather f t (ms, accum) =
+fun amass f t (ms, accum) =
   let val (m, accum) = f t accum in (m :: ms, accum) end
 
-(* hol_context -> bool -> typ -> term list * term list -> bool *)
-fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
-                       (nondef_ts, def_ts) =
+(* string -> bool -> hol_context -> bool -> typ -> term list * term list
+   -> (literal list * (mterm list * mterm list) * (styp * mtyp) list) option *)
+fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
+          (nondef_ts, def_ts) =
   let
-    val _ = print_g ("****** Monotonicity analysis: " ^
+    val _ = print_g ("****** " ^ which ^ " analysis: " ^
                      string_for_mtype MAlpha ^ " is " ^
                      Syntax.string_of_typ ctxt alpha_T)
-    val mdata as {max_fresh, constr_cache, ...} =
-      initial_mdata hol_ctxt binarize alpha_T
-
+    val mdata as {max_fresh, constr_mcache, ...} =
+      initial_mdata hol_ctxt binarize no_harmless alpha_T
     val accum = (initial_gamma, slack)
     val (nondef_ms, accum) =
-      ([], accum) |> gather (consider_general_formula mdata Plus) (hd nondef_ts)
-                  |> fold (gather (consider_nondefinitional_axiom mdata))
+      ([], accum) |> amass (consider_general_formula mdata Plus) (hd nondef_ts)
+                  |> fold (amass (consider_nondefinitional_axiom mdata))
                           (tl nondef_ts)
     val (def_ms, (gamma, cset)) =
-      ([], accum) |> fold (gather (consider_definitional_axiom mdata)) def_ts
+      ([], accum) |> fold (amass (consider_definitional_axiom mdata)) def_ts
   in
     case solve (!max_fresh) cset of
-      SOME lits => (print_mtype_context ctxt lits gamma; true)
-    | _ => false
+      SOME lits => (print_mtype_context ctxt lits gamma;
+                    SOME (lits, (nondef_ms, def_ms), !constr_mcache))
+    | _ => NONE
   end
-  handle MTYPE (loc, Ms) => raise BAD (loc, commas (map string_for_mtype Ms))
+  handle MTYPE (loc, Ms, Ts) =>
+         raise BAD (loc, commas (map string_for_mtype Ms @
+                                 map (Syntax.string_of_typ ctxt) Ts))
+       | MTERM (loc, ms) =>
+         raise BAD (loc, commas (map (string_for_mterm ctxt) ms))
+
+(* hol_context -> bool -> typ -> term list * term list -> bool *)
+val formulas_monotonic = is_some oooo infer "Monotonicity" false
+
+(* typ -> typ -> styp *)
+fun fin_fun_constr T1 T2 =
+  (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
+
+(* hol_context -> bool -> (typ option * bool option) list -> typ
+   -> term list * term list -> term list * term list *)
+fun finitize_funs (hol_ctxt as {thy, stds, fast_descrs, constr_cache, ...})
+                  binarize finitizes alpha_T tsp =
+  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
+    SOME (lits, msp, constr_mtypes) =>
+    let
+      (* typ -> sign_atom -> bool *)
+      fun should_finitize T a =
+        case triple_lookup (type_match thy) finitizes T of
+          SOME (SOME false) => false
+        | _ => resolve_sign_atom lits a = S Plus
+      (* typ -> mtyp -> typ *)
+      fun type_from_mtype T M =
+        case (M, T) of
+          (MAlpha, _) => T
+        | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
+          Type (if should_finitize T a then @{type_name fin_fun}
+                else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
+        | (MPair (M1, M2), Type (@{type_name "*"}, Ts)) =>
+          Type (@{type_name "*"}, map2 type_from_mtype Ts [M1, M2])
+        | (MType _, _) => T
+        | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
+                            [M], [T])
+      (* styp -> styp *)
+      fun finitize_constr (x as (s, T)) =
+        (s, case AList.lookup (op =) constr_mtypes x of
+              SOME M => type_from_mtype T M
+            | NONE => T)
+      (* typ list -> mterm -> term *)
+      fun term_from_mterm Ts m =
+        case m of
+          MRaw (t, M) =>
+          let
+            val T = fastype_of1 (Ts, t)
+            val T' = type_from_mtype T M
+          in
+            case t of
+              Const (x as (s, T)) =>
+              if member (op =) [@{const_name "=="}, @{const_name "op ="}] s then
+                Const (s, T')
+              else if is_built_in_const thy stds fast_descrs x then
+                coerce_term hol_ctxt Ts T' T t
+              else if is_constr thy stds x then
+                Const (finitize_constr x)
+              else if is_sel s then
+                let
+                  val n = sel_no_from_name s
+                  val x' = x |> binarized_and_boxed_constr_for_sel hol_ctxt
+                                                                   binarize
+                             |> finitize_constr
+                  val x'' = binarized_and_boxed_nth_sel_for_constr hol_ctxt
+                                                                   binarize x' n
+                in Const x'' end
+              else
+                Const (s, T')
+            | Free (s, T) => Free (s, type_from_mtype T M)
+            | Bound _ => t
+            | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
+                                [m])
+          end
+        | MAbs (s, T, M, a, m') =>
+          let
+            val T = type_from_mtype T M
+            val t' = term_from_mterm (T :: Ts) m'
+            val T' = fastype_of1 (T :: Ts, t')
+          in
+            Abs (s, T, t')
+            |> should_finitize (T --> T') a
+               ? construct_value thy stds (fin_fun_constr T T') o single
+          end
+        | MApp (m1, m2) =>
+          let
+            val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2)
+            val (T1, T2) = pairself (curry fastype_of1 Ts) (t1, t2)
+            val (t1', T2') =
+              case T1 of
+                Type (s, [T11, T12]) => 
+                (if s = @{type_name fin_fun} then
+                   select_nth_constr_arg thy stds (fin_fun_constr T11 T12) t1 0
+                                         (T11 --> T12)
+                 else
+                   t1, T11)
+              | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
+                                 [T1], [])
+          in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end
+    in
+      Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
+      pairself (map (term_from_mterm [])) msp
+    end
+  | NONE => tsp
 
 end;
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -287,8 +287,9 @@
        "Tuple " ^ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^
        implode (map sub us)
      | Construct (us', T, R, us) =>
-       "Construct " ^ implode (map sub us') ^ Syntax.string_of_typ ctxt T ^
-       " " ^ string_for_rep R ^ " " ^ implode (map sub us)
+       "Construct " ^ implode (map sub us') ^ " " ^
+       Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
+       implode (map sub us)
      | BoundName (j, T, R, nick) =>
        "BoundName " ^ signed_string_of_int j ^ " " ^
        Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^ nick
@@ -459,7 +460,8 @@
       (res_T, Const (@{const_name snd}, T --> res_T) $ t)
     end
 (* typ * term -> (typ * term) list *)
-fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
+fun factorize (z as (Type (@{type_name "*"}, _), _)) =
+    maps factorize [mk_fst z, mk_snd z]
   | factorize z = [z]
 
 (* hol_context -> op2 -> term -> nut *)
@@ -623,7 +625,8 @@
           if is_built_in_const thy stds false x then Cst (Add, T, Any)
           else ConstName (s, T, Any)
         | (Const (@{const_name minus_class.minus},
-                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+                  Type (@{type_name fun},
+                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
            [t1, t2]) =>
           Op2 (SetDifference, T1, Any, sub t1, sub t2)
         | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
@@ -642,7 +645,8 @@
           else
             do_apply t0 ts
         | (Const (@{const_name ord_class.less_eq},
-                  Type ("fun", [Type ("fun", [_, @{typ bool}]), _])),
+                  Type (@{type_name fun},
+                        [Type (@{type_name fun}, [_, @{typ bool}]), _])),
            [t1, t2]) =>
           Op2 (Subset, bool_T, Any, sub t1, sub t2)
         (* FIXME: find out if this case is necessary *)
@@ -666,7 +670,7 @@
         | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
         | (Const (@{const_name is_unknown}, _), [t1]) =>
           Op1 (IsUnknown, bool_T, Any, sub t1)
-        | (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
+        | (Const (@{const_name Tha}, Type (@{type_name fun}, [_, T2])), [t1]) =>
           Op1 (Tha, T2, Any, sub t1)
         | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
         | (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
@@ -676,11 +680,13 @@
                   T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
           Cst (NatToInt, T, Any)
         | (Const (@{const_name semilattice_inf_class.inf},
-                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+                  Type (@{type_name fun},
+                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
            [t1, t2]) =>
           Op2 (Intersect, T1, Any, sub t1, sub t2)
         | (Const (@{const_name semilattice_sup_class.sup},
-                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+                  Type (@{type_name fun},
+                        [T1 as Type (@{type_name fun}, [_, @{typ bool}]), _])),
            [t1, t2]) =>
           Op2 (Union, T1, Any, sub t1, sub t2)
         | (t0 as Const (x as (s, T)), ts) =>
@@ -956,7 +962,7 @@
                  if ok then Cst (Num j, T, Atom (k, j0))
                  else Cst (Unrep, T, Opt (Atom (k, j0)))
                end)
-        | Cst (Suc, T as Type ("fun", [T1, _]), _) =>
+        | Cst (Suc, T as Type (@{type_name fun}, [T1, _]), _) =>
           let val R = Atom (spec_of_type scope T1) in
             Cst (Suc, T, Func (R, Opt R))
           end
@@ -1306,12 +1312,13 @@
   in (w :: ws, pool, NameTable.update (v, w) table) end
 
 (* typ -> rep -> nut list -> nut *)
-fun shape_tuple (T as Type ("*", [T1, T2])) (R as Struct [R1, R2]) us =
+fun shape_tuple (T as Type (@{type_name "*"}, [T1, T2])) (R as Struct [R1, R2])
+                us =
     let val arity1 = arity_of_rep R1 in
       Tuple (T, R, [shape_tuple T1 R1 (List.take (us, arity1)),
                     shape_tuple T2 R2 (List.drop (us, arity1))])
     end
-  | shape_tuple (T as Type ("fun", [_, T2])) (R as Vect (k, R')) us =
+  | shape_tuple (T as Type (@{type_name fun}, [_, T2])) (R as Vect (k, R')) us =
     Tuple (T, R, map (shape_tuple T2 R') (batch_list (length us div k) us))
   | shape_tuple T _ [u] =
     if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -9,7 +9,9 @@
 sig
   type hol_context = Nitpick_HOL.hol_context
   val preprocess_term :
-    hol_context -> term -> term list * term list * bool * bool * bool
+    hol_context -> (typ option * bool option) list
+    -> (typ option * bool option) list -> term
+    -> term list * term list * bool * bool * bool
 end
 
 structure Nitpick_Preproc : NITPICK_PREPROC =
@@ -17,6 +19,7 @@
 
 open Nitpick_Util
 open Nitpick_HOL
+open Nitpick_Mono
 
 (* polarity -> string -> bool *)
 fun is_positive_existential polar quant_s =
@@ -115,88 +118,15 @@
 
 (** Boxing **)
 
-(* hol_context -> typ -> term -> term *)
-fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
-  (case head_of t of
-     Const x => if is_constr_like thy x then t else raise SAME ()
-   | _ => raise SAME ())
-  handle SAME () =>
-         let
-           val x' as (_, T') =
-             if is_pair_type T then
-               let val (T1, T2) = HOLogic.dest_prodT T in
-                 (@{const_name Pair}, T1 --> T2 --> T)
-               end
-             else
-               datatype_constrs hol_ctxt T |> hd
-           val arg_Ts = binder_types T'
-         in
-           list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
-                                     (index_seq 0 (length arg_Ts)) arg_Ts)
-         end
-
-(* (term -> term) -> int -> term -> term *)
-fun coerce_bound_no f j t =
-  case t of
-    t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
-  | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
-  | Bound j' => if j' = j then f t else t
-  | _ => t
-(* hol_context -> typ -> typ -> term -> term *)
-fun coerce_bound_0_in_term hol_ctxt new_T old_T =
-  old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
-(* hol_context -> typ list -> typ -> typ -> term -> term *)
-and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
-  if old_T = new_T then
-    t
-  else
-    case (new_T, old_T) of
-      (Type (new_s, new_Ts as [new_T1, new_T2]),
-       Type ("fun", [old_T1, old_T2])) =>
-      (case eta_expand Ts t 1 of
-         Abs (s, _, t') =>
-         Abs (s, new_T1,
-              t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
-                 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
-         |> Envir.eta_contract
-         |> new_s <> "fun"
-            ? construct_value thy stds
-                  (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
-                  o single
-       | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t']))
-    | (Type (new_s, new_Ts as [new_T1, new_T2]),
-       Type (old_s, old_Ts as [old_T1, old_T2])) =>
-      if old_s = @{type_name fun_box} orelse
-         old_s = @{type_name pair_box} orelse old_s = "*" then
-        case constr_expand hol_ctxt old_T t of
-          Const (old_s, _) $ t1 =>
-          if new_s = "fun" then
-            coerce_term hol_ctxt Ts new_T (Type ("fun", old_Ts)) t1
-          else
-            construct_value thy stds
-                (old_s, Type ("fun", new_Ts) --> new_T)
-                [coerce_term hol_ctxt Ts (Type ("fun", new_Ts))
-                             (Type ("fun", old_Ts)) t1]
-        | Const _ $ t1 $ t2 =>
-          construct_value thy stds
-              (if new_s = "*" then @{const_name Pair}
-               else @{const_name PairBox}, new_Ts ---> new_T)
-              [coerce_term hol_ctxt Ts new_T1 old_T1 t1,
-               coerce_term hol_ctxt Ts new_T2 old_T2 t2]
-        | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t'])
-      else
-        raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
-    | _ => raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
-
 (* hol_context -> bool -> term -> term *)
 fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
                              orig_t =
   let
     (* typ -> typ *)
-    fun box_relational_operator_type (Type ("fun", Ts)) =
-        Type ("fun", map box_relational_operator_type Ts)
-      | box_relational_operator_type (Type ("*", Ts)) =
-        Type ("*", map (box_type hol_ctxt InPair) Ts)
+    fun box_relational_operator_type (Type (@{type_name fun}, Ts)) =
+        Type (@{type_name fun}, map box_relational_operator_type Ts)
+      | box_relational_operator_type (Type (@{type_name "*"}, Ts)) =
+        Type (@{type_name "*"}, map (box_type hol_ctxt InPair) Ts)
       | box_relational_operator_type T = T
     (* indexname * typ -> typ * term -> typ option list -> typ option list *)
     fun add_boxed_types_for_var (z as (_, T)) (T', t') =
@@ -320,12 +250,13 @@
           val T2 = fastype_of1 (new_Ts, t2)
           val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
         in
-          betapply (if s1 = "fun" then
+          betapply (if s1 = @{type_name fun} then
                       t1
                     else
                       select_nth_constr_arg thy stds
-                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
-                          (Type ("fun", Ts1)), t2)
+                          (@{const_name FunBox},
+                           Type (@{type_name fun}, Ts1) --> T1) t1 0
+                          (Type (@{type_name fun}, Ts1)), t2)
         end
       | t1 $ t2 =>
         let
@@ -336,12 +267,13 @@
           val T2 = fastype_of1 (new_Ts, t2)
           val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
         in
-          betapply (if s1 = "fun" then
+          betapply (if s1 = @{type_name fun} then
                       t1
                     else
                       select_nth_constr_arg thy stds
-                          (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
-                          (Type ("fun", Ts1)), t2)
+                          (@{const_name FunBox},
+                           Type (@{type_name fun}, Ts1) --> T1) t1 0
+                          (Type (@{type_name fun}, Ts1)), t2)
         end
       | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
       | Var (z as (x, T)) =>
@@ -597,7 +529,7 @@
                if pass1 then do_eq false t2 t1 else raise SAME ()
              else case t1 of
                Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
-             | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
+             | Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' =>
                if j' = j andalso
                   s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
                  SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
@@ -1141,8 +1073,8 @@
     (* int -> typ -> accumulator -> accumulator *)
     and add_axioms_for_type depth T =
       case T of
-        Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
-      | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
+        Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
+      | Type (@{type_name "*"}, Ts) => fold (add_axioms_for_type depth) Ts
       | @{typ prop} => I
       | @{typ bool} => I
       | @{typ unit} => I
@@ -1399,11 +1331,29 @@
              | _ => t
   in aux "" [] [] end
 
+(** Inference of finite functions **)
+
+(* hol_context -> bool -> (typ option * bool option) list
+   -> (typ option * bool option) list -> term list * term list
+   -> term list * term list *)
+fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
+                               (nondef_ts, def_ts) =
+  let
+    val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
+             |> filter_out (fn Type (@{type_name fun_box}, _) => true
+                             | T => is_small_finite_type hol_ctxt T orelse
+                                    triple_lookup (type_match thy) monos T
+                                    = SOME (SOME false))
+  in fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) end
+
 (** Preprocessor entry point **)
 
-(* hol_context -> term -> term list * term list * bool * bool * bool *)
+(* hol_context -> (typ option * bool option) list
+   -> (typ option * bool option) list -> term
+   -> term list * term list * bool * bool * bool *)
 fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
-                                  boxes, skolemize, uncurry, ...}) t =
+                                  boxes, skolemize, uncurry, ...})
+                    finitizes monos t =
   let
     val skolem_depth = if skolemize then 4 else ~1
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
@@ -1442,6 +1392,9 @@
       #> Term.map_abs_vars shortest_name
     val nondef_ts = map (do_rest false) nondef_ts
     val def_ts = map (do_rest true) def_ts
+    val (nondef_ts, def_ts) =
+      finitize_all_types_of_funs hol_ctxt binarize finitizes monos
+                                 (nondef_ts, def_ts)
   in
     (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
   end
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/nitpick_rep.ML
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -158,9 +158,9 @@
   | smart_range_rep _ _ _ (Func (_, R2)) = R2
   | smart_range_rep ofs T ran_card (Opt R) =
     Opt (smart_range_rep ofs T ran_card R)
-  | smart_range_rep ofs (Type ("fun", [_, T2])) _ (Atom (1, _)) =
+  | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) _ (Atom (1, _)) =
     Atom (1, offset_of_type ofs T2)
-  | smart_range_rep ofs (Type ("fun", [_, T2])) ran_card (Atom _) =
+  | smart_range_rep ofs (Type (@{type_name fun}, [_, T2])) ran_card (Atom _) =
     Atom (ran_card (), offset_of_type ofs T2)
   | smart_range_rep _ _ _ R = raise REP ("Nitpick_Rep.smart_range_rep", [R])
 
@@ -183,10 +183,10 @@
   | one_rep _ _ (Vect z) = Vect z
   | one_rep ofs T (Opt R) = one_rep ofs T R
   | one_rep ofs T R = Atom (card_of_rep R, offset_of_type ofs T)
-fun optable_rep ofs (Type ("fun", [_, T2])) (Func (R1, R2)) =
+fun optable_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
     Func (R1, optable_rep ofs T2 R2)
   | optable_rep ofs T R = one_rep ofs T R
-fun opt_rep ofs (Type ("fun", [_, T2])) (Func (R1, R2)) =
+fun opt_rep ofs (Type (@{type_name fun}, [_, T2])) (Func (R1, R2)) =
     Func (R1, opt_rep ofs T2 R2)
   | opt_rep ofs T R = Opt (optable_rep ofs T R)
 (* rep -> rep *)
@@ -264,11 +264,11 @@
 
 (* scope -> typ -> rep *)
 fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)
-                          (Type ("fun", [T1, T2])) =
+                          (Type (@{type_name fun}, [T1, T2])) =
     (case best_one_rep_for_type scope T2 of
        Unit => Unit
      | R2 => Vect (card_of_type card_assigns T1, R2))
-  | best_one_rep_for_type scope (Type ("*", [T1, T2])) =
+  | best_one_rep_for_type scope (Type (@{type_name "*"}, [T1, T2])) =
     (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
        (Unit, Unit) => Unit
      | (R1, R2) => Struct [R1, R2])
@@ -284,12 +284,12 @@
 (* Datatypes are never represented by Unit, because it would confuse
    "nfa_transitions_for_ctor". *)
 (* scope -> typ -> rep *)
-fun best_opt_set_rep_for_type scope (Type ("fun", [T1, T2])) =
+fun best_opt_set_rep_for_type scope (Type (@{type_name fun}, [T1, T2])) =
     Func (best_one_rep_for_type scope T1, best_opt_set_rep_for_type scope T2)
   | best_opt_set_rep_for_type (scope as {ofs, ...}) T =
     opt_rep ofs T (best_one_rep_for_type scope T)
 fun best_non_opt_set_rep_for_type (scope as {ofs, ...})
-                                  (Type ("fun", [T1, T2])) =
+                                  (Type (@{type_name fun}, [T1, T2])) =
     (case (best_one_rep_for_type scope T1,
            best_non_opt_set_rep_for_type scope T2) of
        (_, Unit) => Unit
@@ -302,7 +302,7 @@
   (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
    else best_opt_set_rep_for_type) scope T
 fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
-                                             (Type ("fun", [T1, T2])) =
+                                           (Type (@{type_name fun}, [T1, T2])) =
     (optable_rep ofs T1 (best_one_rep_for_type scope T1),
      optable_rep ofs T2 (best_one_rep_for_type scope T2))
   | best_non_opt_symmetric_reps_for_fun_type _ T =
@@ -325,11 +325,11 @@
 fun type_schema_of_rep _ (Formula _) = []
   | type_schema_of_rep _ Unit = []
   | type_schema_of_rep T (Atom _) = [T]
-  | type_schema_of_rep (Type ("*", [T1, T2])) (Struct [R1, R2]) =
+  | type_schema_of_rep (Type (@{type_name "*"}, [T1, T2])) (Struct [R1, R2]) =
     type_schema_of_reps [T1, T2] [R1, R2]
-  | type_schema_of_rep (Type ("fun", [_, T2])) (Vect (k, R)) =
+  | type_schema_of_rep (Type (@{type_name fun}, [_, T2])) (Vect (k, R)) =
     replicate_list k (type_schema_of_rep T2 R)
-  | type_schema_of_rep (Type ("fun", [T1, T2])) (Func (R1, R2)) =
+  | type_schema_of_rep (Type (@{type_name fun}, [T1, T2])) (Func (R1, R2)) =
     type_schema_of_rep T1 R1 @ type_schema_of_rep T2 R2
   | type_schema_of_rep T (Opt R) = type_schema_of_rep T R
   | type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
diff -r fee01e85605f -r ff2bf50505ab src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Mar 08 15:20:40 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Mar 09 09:25:23 2010 +0100
@@ -106,22 +106,26 @@
     | NONE => constr_spec dtypes x
 
 (* dtype_spec list -> bool -> typ -> bool *)
-fun is_complete_type dtypes facto (Type ("fun", [T1, T2])) =
+fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
     is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
-  | is_complete_type dtypes facto (Type ("*", Ts)) =
+  | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
+    is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
+  | is_complete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
     forall (is_complete_type dtypes facto) Ts
   | is_complete_type dtypes facto T =
     not (is_integer_like_type T) andalso not (is_bit_type T) andalso
     fun_from_pair (#complete (the (datatype_spec dtypes T))) facto
     handle Option.Option => true
-and is_concrete_type dtypes facto (Type ("fun", [T1, T2])) =
+and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
     is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
-  | is_concrete_type dtypes facto (Type ("*", Ts)) =
+  | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
+    is_concrete_type dtypes facto T2
+  | is_concrete_type dtypes facto (Type (@{type_name "*"}, Ts)) =
     forall (is_concrete_type dtypes facto) Ts
   | is_concrete_type dtypes facto T =
     fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
     handle Option.Option => true
-fun is_exact_type dtypes facto =
+and is_exact_type dtypes facto =
   is_complete_type dtypes facto andf is_concrete_type dtypes facto
 
 (* int Typtab.table -> typ -> int *)
@@ -528,15 +532,15 @@
 
 (* theory -> typ list -> (typ option * int list) list
    -> (typ option * int list) list *)
-fun repair_cards_assigns_wrt_boxing _ _ [] = []
-  | repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
+fun repair_cards_assigns_wrt_boxing_etc _ _ [] = []
+  | repair_cards_assigns_wrt_boxing_etc 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 unarize_and_unbox_type)
-          |> map (rpair ks o SOME)
+       Ts |> filter (curry (type_match thy o swap) T) |> map (rpair ks o SOME)
      else
-       [(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns
-  | repair_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) =
-    (NONE, ks) :: repair_cards_assigns_wrt_boxing thy Ts cards_assigns
+       [(SOME T, ks)]) @
+       repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
+  | repair_cards_assigns_wrt_boxing_etc thy Ts ((NONE, ks) :: cards_assigns) =
+    (NONE, ks) :: repair_cards_assigns_wrt_boxing_etc thy Ts cards_assigns
 
 val max_scopes = 4096
 val distinct_threshold = 512
@@ -548,8 +552,8 @@
                maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
                deep_dataTs finitizable_dataTs =
   let
-    val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
-                                                        cards_assigns
+    val cards_assigns = repair_cards_assigns_wrt_boxing_etc thy mono_Ts
+                                                            cards_assigns
     val blocks = blocks_for_types hol_ctxt binarize cards_assigns maxes_assigns
                                   iters_assigns bitss bisim_depths mono_Ts
                                   nonmono_Ts