# HG changeset patch
# User blanchet
# Date 1291720213 -3600
# Node ID d6f45159ae84241eef6cf3eb6f953178f90b3cab
# Parent  1c0eefa8d02a2bf8165568d9c3f007923d6f4281# Parent  e58d1cdda832eb8fd75d62c9be64cc79eb307c47
merged

diff -r 1c0eefa8d02a -r d6f45159ae84 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Tue Dec 07 11:50:16 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Tue Dec 07 12:10:13 2010 +0100
@@ -2108,14 +2108,9 @@
 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:
+Specifies whether Nitpick should attempt to finitize an infinite ``shallow
+datatype'' (an infinite datatype whose constructors don't appear in the
+problem). The option can then take the following values:
 
 \begin{enum}
 \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type.
@@ -2132,12 +2127,9 @@
 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.
+detect whether the datatype can be soundly 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
diff -r 1c0eefa8d02a -r d6f45159ae84 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Tue Dec 07 11:50:16 2010 +0100
+++ b/src/HOL/Nitpick.thy	Tue Dec 07 12:10:13 2010 +0100
@@ -35,7 +35,6 @@
            and Quot :: "'a \<Rightarrow> 'b"
            and safe_The :: "('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
 
@@ -76,6 +75,9 @@
 "tranclp r a b \<equiv> trancl (split r) (a, b)"
 by (simp add: trancl_def Collect_def mem_def)
 
+definition prod :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
+"prod A B = {(a, b). a \<in> A \<and> b \<in> B}"
+
 definition refl' :: "('a \<times> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
 "refl' r \<equiv> \<forall>x. (x, x) \<in> r"
 
@@ -237,18 +239,17 @@
 setup {* Nitpick_Isar.setup *}
 
 hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
-    FinFun FunBox PairBox Word refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
+    FunBox PairBox Word prod 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_frac less_eq_frac of_frac
-hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
-    word
-hide_fact (open) 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
-    nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
-    num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def
-    uminus_frac_def number_of_frac_def inverse_frac_def less_frac_def
-    less_eq_frac_def of_frac_def
+hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
+hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def prod_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 nat_lcm_def int_gcd_def int_lcm_def Frac_def
+    zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
+    plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
+    inverse_frac_def less_frac_def less_eq_frac_def of_frac_def
 
 end
diff -r 1c0eefa8d02a -r d6f45159ae84 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Dec 07 11:50:16 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Dec 07 12:10:13 2010 +0100
@@ -67,7 +67,6 @@
 ML {* Nitpick_Mono.trace := false *}
 
 ML {* const @{term "A\<Colon>('a\<Rightarrow>'b)"} *}
-(*
 ML {* const @{term "(A\<Colon>'a set) = A"} *}
 ML {* const @{term "(A\<Colon>'a set set) = A"} *}
 ML {* const @{term "(\<lambda>x\<Colon>'a set. x a)"} *}
@@ -138,7 +137,6 @@
 
 ML {* nonmono @{prop "A = (\<lambda>x::'a. True) \<and> A = (\<lambda>x. False)"} *}
 ML {* nonmono @{prop "\<forall>F f g (h\<Colon>'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
-*)
 
 ML {*
 val preproc_timeout = SOME (seconds 5.0)
@@ -184,8 +182,6 @@
 
 fun check_theory thy =
   let
-    val finitizes = [(NONE, SOME false)]
-    val monos = [(NONE, SOME false)]
     val path = File.tmp_path (Context.theory_name thy ^ ".out" |> Path.explode)
     val _ = File.write path ""
     fun check_theorem (name, th) =
@@ -193,8 +189,7 @@
         val t = th |> prop_of |> Type.legacy_freeze |> close_form
         val neg_t = Logic.mk_implies (t, @{prop False})
         val (nondef_ts, def_ts, _, _, _) =
-          time_limit preproc_timeout
-              (preprocess_formulas hol_ctxt finitizes monos []) neg_t
+          time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
         val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
       in File.append path (res ^ "\n"); writeln res end
       handle TimeLimit.TimeOut => ()
diff -r 1c0eefa8d02a -r d6f45159ae84 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:50:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 12:10:13 2010 +0100
@@ -179,6 +179,10 @@
 
 fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
 
+fun has_lonely_bool_var (@{const Pure.conjunction}
+                         $ (@{const Trueprop} $ Free _) $ _) = true
+  | has_lonely_bool_var _ = false
+
 val syntactic_sorts =
   @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
   @{sort number}
@@ -229,8 +233,7 @@
     val print_v = pprint_v o K o plazy
 
     fun check_deadline () =
-      if debug andalso passed_deadline deadline then raise TimeLimit.TimeOut
-      else ()
+      if passed_deadline deadline then raise TimeLimit.TimeOut else ()
 
     val assm_ts = if assms orelse auto then assm_ts else []
     val _ =
@@ -289,7 +292,7 @@
     val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
             raise NOT_SUPPORTED "schematic type variables"
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
-         binarize) = preprocess_formulas hol_ctxt finitizes monos assm_ts neg_t
+         binarize) = preprocess_formulas hol_ctxt assm_ts neg_t
     val got_all_user_axioms =
       got_all_mono_user_axioms andalso no_poly_user_axioms
 
@@ -358,9 +361,7 @@
         SOME (SOME b) => b
       | _ => 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}, _)) =
+    fun 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
@@ -661,7 +662,9 @@
                     \section for details (\"isabelle doc nitpick\")."
             else
               ();
-            if has_syntactic_sorts orig_t then
+            if has_lonely_bool_var orig_t then
+              print "Hint: Maybe you forgot a colon after the lemma's name?"
+            else if has_syntactic_sorts orig_t then
               print "Hint: Maybe you forgot a type constraint?"
             else
               ();
@@ -975,6 +978,9 @@
                 ".")
   in (outcome_code, !state_ref) end
 
+(* Give the inner timeout a chance. *)
+val timeout_bonus = seconds 0.25
+
 fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
                       step subst assm_ts orig_t =
   let val warning_m = if auto then K () else warning in
@@ -988,7 +994,8 @@
         val unknown_outcome = ("unknown", state)
         val deadline = Option.map (curry Time.+ (Time.now ())) timeout
         val outcome as (outcome_code, _) =
-          time_limit (if debug then NONE else timeout)
+          time_limit (if debug orelse is_none timeout then NONE
+                      else SOME (Time.+ (the timeout, timeout_bonus)))
               (pick_them_nits_in_term deadline state params auto i n step subst
                                       assm_ts) orig_t
           handle TOO_LARGE (_, details) =>
diff -r 1c0eefa8d02a -r d6f45159ae84 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:50:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 12:10:13 2010 +0100
@@ -65,6 +65,7 @@
   val strip_first_name_sep : string -> string * string
   val original_name : string -> string
   val abs_var : indexname * typ -> term -> term
+  val is_higher_order_type : typ -> bool
   val s_let : string -> int -> typ -> typ -> (term -> term) -> term -> term
   val s_betapply : typ list -> term * term -> term
   val s_betapplys : typ list -> term * term list -> term
@@ -87,7 +88,6 @@
   val term_match : theory -> term * term -> bool
   val frac_from_term_pair : typ -> term -> term -> term
   val is_TFree : typ -> bool
-  val is_higher_order_type : typ -> bool
   val is_fun_type : typ -> bool
   val is_set_type : typ -> bool
   val is_pair_type : typ -> bool
@@ -319,13 +319,18 @@
   else
     s
 
+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 abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
 
 fun let_var s = (nitpick_prefix ^ s, 999)
 val let_inline_threshold = 20
 
 fun s_let s n abs_T body_T f t =
-  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold then
+  if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
+     is_higher_order_type abs_T then
     f t
   else
     let val z = (let_var s, abs_T) in
@@ -419,7 +424,6 @@
    (@{const_name converse}, 1),
    (@{const_name trancl}, 1),
    (@{const_name rel_comp}, 2),
-   (@{const_name image}, 2),
    (@{const_name finite}, 1),
    (@{const_name unknown}, 0),
    (@{const_name is_unknown}, 1),
@@ -458,9 +462,7 @@
   | 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_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)) =
+fun 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 prod}, map unarize_unbox_etc_type Ts)
@@ -512,9 +514,6 @@
 
 fun is_TFree (TFree _) = true
   | is_TFree _ = false
-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 (@{type_name fun}, _)) = true
   | is_fun_type _ = false
 fun is_set_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
@@ -803,9 +802,9 @@
     end
   | _ => false
 fun is_constr_like ctxt (s, T) =
-  member (op =) [@{const_name FinFun}, @{const_name FunBox},
-                 @{const_name PairBox}, @{const_name Quot},
-                 @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
+  member (op =) [@{const_name FunBox}, @{const_name PairBox},
+                 @{const_name Quot}, @{const_name Zero_Rep},
+                 @{const_name Suc_Rep}] s orelse
   let
     val thy = ProofContext.theory_of ctxt
     val (x as (_, T)) = (s, unarize_unbox_etc_type T)
@@ -1094,14 +1093,13 @@
          |> Envir.eta_contract
          |> new_s <> @{type_name fun}
             ? construct_value ctxt stds
-                  (if new_s = @{type_name fin_fun} then @{const_name FinFun}
-                   else @{const_name FunBox},
+                  (@{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
+      if old_s = @{type_name fun_box} orelse
          old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then
         case constr_expand hol_ctxt old_T t of
           Const (old_s, _) $ t1 =>
@@ -1643,9 +1641,14 @@
                 s_betapply [] (do_term depth Ts t0, do_term depth Ts t1))
       | Const (@{const_name refl_on}, T) $ Const (@{const_name top}, _) $ t2 =>
         do_const depth Ts t (@{const_name refl'}, range_type T) [t2]
-      | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
-        s_betapplys Ts (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
-                        map (do_term depth Ts) [t1, t2])
+      | (t0 as Const (@{const_name Sigma}, Type (_, [T1, Type (_, [T2, T3])])))
+        $ t1 $ (t2 as Abs (_, _, t2')) =>
+        if loose_bvar1 (t2', 0) then
+          s_betapplys Ts (do_term depth Ts t0, map (do_term depth Ts) [t1, t2])
+        else
+          do_term depth Ts
+                  (Const (@{const_name prod}, T1 --> range_type T2 --> T3)
+                   $ t1 $ incr_boundvars ~1 t2')
       | Const (x as (@{const_name distinct},
                Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
         $ (t1 as _ $ _) =>
@@ -1658,6 +1661,8 @@
           do_term depth Ts t2
         else
           do_const depth Ts t x [t1, t2, t3]
+      | Const (@{const_name Let}, _) $ t1 $ t2 =>
+        s_betapply Ts (pairself (do_term depth Ts) (t2, t1))
       | Const x => do_const depth Ts t x []
       | t1 $ t2 =>
         (case strip_comb t of
diff -r 1c0eefa8d02a -r d6f45159ae84 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Dec 07 11:50:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Dec 07 12:10:13 2010 +0100
@@ -99,7 +99,7 @@
                         ""
                       else
                         " of Kodkod relation associated with " ^
-                        quote guilty_party) ^
+                        quote (original_name guilty_party)) ^
                      " too large for universe of cardinality " ^
                      string_of_int univ_card)
   else
@@ -1510,55 +1510,6 @@
            | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))
           |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))
         end
-      | Op2 (Product, T, R, u1, u2) =>
-        let
-          val (a_T, b_T) = HOLogic.dest_prodT (domain_type T)
-          val a_k = card_of_domain_from_rep 2 (rep_of u1)
-          val b_k = card_of_domain_from_rep 2 (rep_of u2)
-          val a_R = Atom (a_k, offset_of_type ofs a_T)
-          val b_R = Atom (b_k, offset_of_type ofs b_T)
-          val body_R = body_rep R
-        in
-          (case body_R of
-             Formula Neut =>
-             kk_product (to_rep (Func (a_R, Formula Neut)) u1)
-                        (to_rep (Func (b_R, Formula Neut)) u2)
-           | Opt (Atom (2, _)) =>
-             let
-               fun do_nut r R u = kk_join (to_rep (Func (R, body_R)) u) r
-               fun do_term r =
-                 kk_product (kk_product (do_nut r a_R u1) (do_nut r b_R u2)) r
-             in kk_union (do_term true_atom) (do_term false_atom) end
-           | _ => raise NUT ("Nitpick_Kodkod.to_r (Product)", [u]))
-          |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, b_R], body_R))
-        end
-      | Op2 (Image, T, R, u1, u2) =>
-        (case (rep_of u1, rep_of u2) of
-           (Func (R11, R12), Func (R21, Formula Neut)) =>
-           if R21 = R11 andalso is_lone_rep R12 then
-             let
-               fun big_join r = kk_n_fold_join kk false R21 R12 r (to_r u1)
-               val core_r = big_join (to_r u2)
-               val core_R = Func (R12, Formula Neut)
-             in
-               if is_opt_rep R12 then
-                 let
-                   val schema = atom_schema_of_rep R21
-                   val decls = decls_for_atom_schema ~1 schema
-                   val vars = unary_var_seq ~1 (length decls)
-                   val f = kk_some (big_join (fold1 kk_product vars))
-                 in
-                   kk_rel_if (kk_all decls f)
-                             (rel_expr_from_rel_expr kk R core_R core_r)
-                             (rel_expr_from_rel_expr kk R (opt_rep ofs T core_R)
-                                              (kk_product core_r true_atom))
-                 end
-               else
-                 rel_expr_from_rel_expr kk R core_R core_r
-             end
-           else
-             raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2])
-         | _ => raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2]))
       | Op2 (Apply, @{typ nat}, _,
              Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) =>
         if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
diff -r 1c0eefa8d02a -r d6f45159ae84 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Dec 07 11:50:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Dec 07 12:10:13 2010 +0100
@@ -178,9 +178,7 @@
 fun tuple_list_for_name rel_table bounds name =
   the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
 
-fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
-    unarize_unbox_etc_term t1
-  | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
+fun unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
     unarize_unbox_etc_term t1
   | unarize_unbox_etc_term
         (Const (@{const_name PairBox},
@@ -559,9 +557,8 @@
                   if length arg_Ts = 0 then
                     []
                   else
-                    map3 (fn Ts =>
-                             term_for_rep (constr_s <> @{const_name FinFun})
-                                          seen Ts Ts) arg_Ts arg_Rs arg_jsss
+                    map3 (fn Ts => term_for_rep true 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 =
@@ -935,8 +932,7 @@
       Pretty.block (Pretty.breaks
           (pretty_for_type ctxt typ ::
            (case typ of
-              Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
-            | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
+              Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
             | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
             | _ => []) @
            [Pretty.str "=",
diff -r 1c0eefa8d02a -r d6f45159ae84 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:50:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 12:10:13 2010 +0100
@@ -12,9 +12,6 @@
   val trace : bool Unsynchronized.ref
   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 =
@@ -41,23 +38,16 @@
   MType of string * mtyp list |
   MRec of string * typ list
 
-datatype mterm =
-  MRaw of term * mtyp |
-  MAbs of string * typ * mtyp * annotation_atom * mterm |
-  MApp of mterm * mterm
-
 type mdata =
   {hol_ctxt: hol_context,
    binarize: bool,
    alpha_T: typ,
-   no_harmless: bool,
    max_fresh: int Unsynchronized.ref,
    datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
    constr_mcache: (styp * mtyp) list Unsynchronized.ref}
 
 exception UNSOLVABLE of unit
 exception MTYPE of string * mtyp list * typ list
-exception MTERM of string * mterm list
 
 val trace = Unsynchronized.ref false
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
@@ -129,43 +119,9 @@
   | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
   | flatten_mtype M = [M]
 
-fun precedence_of_mterm (MRaw _) = no_prec
-  | precedence_of_mterm (MAbs _) = 1
-  | precedence_of_mterm (MApp _) = 2
-
-fun string_for_mterm ctxt =
-  let
-    fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
-    fun aux outer_prec m =
-      let
-        val prec = precedence_of_mterm m
-        val need_parens = (prec < outer_prec)
-      in
-        (if need_parens then "(" else "") ^
-        (case m of
-           MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
-         | MAbs (s, _, M, aa, m) =>
-           "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
-           string_for_annotation_atom aa ^ "\<^esup> " ^ aux prec m
-         | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
-        (if need_parens then ")" else "")
-      end
-  in aux 0 end
-
-fun mtype_of_mterm (MRaw (_, M)) = M
-  | mtype_of_mterm (MAbs (_, _, M, aa, m)) = MFun (M, aa, mtype_of_mterm m)
-  | mtype_of_mterm (MApp (m1, _)) =
-    case mtype_of_mterm m1 of
-      MFun (_, _, M12) => M12
-    | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1], [])
-
-fun strip_mcomb (MApp (m1, m2)) = strip_mcomb m1 ||> (fn ms => append ms [m2])
-  | strip_mcomb m = (m, [])
-
-fun initial_mdata hol_ctxt binarize no_harmless alpha_T =
+fun initial_mdata hol_ctxt binarize alpha_T =
   ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
-    no_harmless = no_harmless, max_fresh = Unsynchronized.ref 0,
-    datatype_mcache = Unsynchronized.ref [],
+    max_fresh = Unsynchronized.ref 0, datatype_mcache = Unsynchronized.ref [],
     constr_mcache = Unsynchronized.ref []} : mdata)
 
 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
@@ -246,7 +202,7 @@
                 $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
   | fin_fun_body _ _ _ = NONE
 
-(* ### FIXME: make sure well-annotated! *)
+(* FIXME: make sure well-annotated *)
 
 fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
                             T1 T2 =
@@ -309,7 +265,8 @@
       | _ => MType (simple_string_of_typ T, [])
   in do_type end
 
-val ground_and_sole_base_constrs = [] (* FIXME: [@{const_name Nil}, @{const_name None}], cf. lists_empty *)
+val ground_and_sole_base_constrs = []
+(* FIXME: [@{const_name Nil}, @{const_name None}], cf. lists_empty *)
 
 fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
   | prodM_factors M = [M]
@@ -647,8 +604,6 @@
   {bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame, frees = frees,
    consts = consts}
 
-(* FIXME: make sure tracing messages are complete *)
-
 fun add_comp_frame aa cmp = fold (add_annotation_atom_comp cmp [] aa o snd)
 
 fun add_bound_frame j frame =
@@ -694,11 +649,11 @@
    [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))],
    [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]]
 
-val meta_conj_triple = ("\<and>", conj_clauses, @{const Pure.conjunction})
-val meta_imp_triple = ("\<implies>", imp_clauses, @{const "==>"})
-val conj_triple = ("\<and>", conj_clauses, @{const conj})
-val disj_triple = ("\<or>", disj_clauses, @{const disj})
-val imp_triple = ("\<implies>", imp_clauses, @{const implies})
+val meta_conj_spec = ("\<and>", conj_clauses)
+val meta_imp_spec = ("\<implies>", imp_clauses)
+val conj_spec = ("\<and>", conj_clauses)
+val disj_spec = ("\<or>", disj_clauses)
+val imp_spec = ("\<implies>", imp_clauses)
 
 fun add_annotation_clause_from_quasi_clause _ NONE = NONE
   | add_annotation_clause_from_quasi_clause [] accum = accum
@@ -764,19 +719,17 @@
     #> fold add_arg_order1 (tl arg_frame ~~ (fst (split_last arg_frame)))
     #> fold (add_app1 fun_aa) (res_frame ~~ arg_frame)
 
-fun consider_connective mdata (conn, mk_quasi_clauses, t0) do_t1 do_t2
+fun consider_connective mdata (conn, mk_quasi_clauses) do_t1 do_t2
                         (accum as ({frame, ...}, _)) =
   let
-    val mtype_for = fresh_mtype_for_type mdata false
     val frame1 = fresh_frame mdata (SOME Tru) NONE frame
     val frame2 = fresh_frame mdata (SOME Fls) NONE frame
-    val (m1, accum) = accum |>> set_frame frame1 |> do_t1
-    val (m2, accum) = accum |>> set_frame frame2 |> do_t2
   in
-    (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
-     accum |>> set_frame frame
-           ||> apsnd (add_connective_frames conn mk_quasi_clauses frame frame1
-                                            frame2))
+    accum |>> set_frame frame1 |> do_t1
+          |>> set_frame frame2 |> do_t2
+          |>> set_frame frame
+          ||> apsnd (add_connective_frames conn mk_quasi_clauses frame frame1
+                                           frame2)
   end
 
 fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, ...}, alpha_T,
@@ -837,8 +790,9 @@
         M as MPair (a_M, b_M) =>
         pair (MFun (M, A Gen, if n = 0 then a_M else b_M))
       | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M], [])
-    and do_connect triple t1 t2 =
-      consider_connective mdata triple (do_term t1) (do_term t2)
+    and do_connect spec t1 t2 accum =
+      (bool_M, consider_connective mdata spec (snd o do_term t1)
+                                   (snd o do_term t2) accum)
     and do_term t
             (accum as (gamma as {bound_Ts, bound_Ms, frame, frees, consts},
                        cset)) =
@@ -846,12 +800,10 @@
                            " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
                            " : _?");
        case t of
-         @{const False} =>
-         (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
+         @{const False} => (bool_M, accum ||> add_comp_frame (A Fls) Leq frame)
        | Const (@{const_name None}, T) =>
-         (MRaw (t, mtype_for T), accum ||> add_comp_frame (A Fls) Leq frame)
-       | @{const True} =>
-         (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
+         (mtype_for T, accum ||> add_comp_frame (A Fls) Leq frame)
+       | @{const True} => (bool_M, accum ||> add_comp_frame (A Tru) Leq frame)
        | (t0 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t2 =>
          (* hack to exploit symmetry of equality when typing "insert" *)
          (if t2 = Bound 0 then do_term @{term True}
@@ -873,7 +825,6 @@
                                   (Abs (Name.uu, domain_type set_T,
                                         @{const False}),
                                    Bound 0)))) accum
-                |>> mtype_of_mterm
               end
             | @{const_name HOL.eq} => do_equals T accum
             | @{const_name The} =>
@@ -912,36 +863,22 @@
                 (MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
                  accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
               end
-            | @{const_name image} =>
-              let
-                val x = Unsynchronized.inc max_fresh
-                val a_M = mtype_for (domain_type (domain_type T))
-                val b_M = mtype_for (range_type (domain_type T))
-              in
-                (MFun (MFun (a_M, A Gen, b_M), A Gen,
-                       MFun (MFun (a_M, V x, bool_M), A Gen,
-                             MFun (b_M, V x, bool_M))),
-                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
-              end
             | @{const_name finite} =>
               let
                 val M1 = mtype_for (domain_type (domain_type T))
                 val a = if exists_alpha_sub_mtype M1 then Fls else Gen
               in (MFun (MFun (M1, A a, bool_M), A Gen, bool_M), accum) end
-            | @{const_name Sigma} =>
+            | @{const_name prod} =>
               let
                 val x = Unsynchronized.inc max_fresh
                 fun mtype_for_set T =
                   MFun (mtype_for (domain_type T), V x, bool_M)
-                val a_set_T = domain_type T
-                val a_M = mtype_for (domain_type a_set_T)
+                val a_set_M = mtype_for_set (domain_type T)
                 val b_set_M =
                   mtype_for_set (range_type (domain_type (range_type T)))
-                val a_set_M = mtype_for_set a_set_T
-                val a_to_b_set_M = MFun (a_M, A Gen, b_set_M)
                 val ab_set_M = mtype_for_set (nth_range_type 2 T)
               in
-                (MFun (a_set_M, A Gen, MFun (a_to_b_set_M, A Gen, ab_set_M)),
+                (MFun (a_set_M, A Gen, MFun (b_set_M, A Gen, ab_set_M)),
                  accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
               end
             | _ =>
@@ -964,7 +901,6 @@
                   (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame,
                         frees = frees, consts = (x, M) :: consts}, cset))
                 end)
-           |>> curry MRaw t
            ||> apsnd (add_comp_frame (A Gen) Eq frame)
          | Free (x as (_, T)) =>
            (case AList.lookup (op =) frees x of
@@ -974,20 +910,20 @@
                 (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms, frame = frame,
                       frees = (x, M) :: frees, consts = consts}, cset))
               end)
-           |>> curry MRaw t ||> apsnd (add_comp_frame (A Gen) Eq frame)
+           ||> apsnd (add_comp_frame (A Gen) Eq frame)
          | Var _ => (trace_msg (K "*** Var"); raise UNSOLVABLE ())
          | Bound j =>
-           (MRaw (t, nth bound_Ms j),
+           (nth bound_Ms j,
             accum ||> add_bound_frame (length bound_Ts - j - 1) frame)
-         | Abs (s, T, t') =>
+         | Abs (_, T, t') =>
            (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
               SOME t' =>
               let
                 val M = mtype_for T
                 val x = Unsynchronized.inc max_fresh
-                val (m', accum) = do_term t' (accum |>> push_bound (V x) T M)
+                val (M', accum) = do_term t' (accum |>> push_bound (V x) T M)
               in
-                (MAbs (s, T, M, V x, m'),
+                (MFun (M, V x, M'),
                  accum |>> pop_bound
                        ||> add_annotation_atom_comp Leq [] (A Fls) (V x))
               end
@@ -1009,13 +945,13 @@
                       let
                         val M = mtype_for T
                         val x = Unsynchronized.inc max_fresh
-                        val (m', accum) =
+                        val (M', accum) =
                           do_term t' (accum |>> push_bound (V x) T M)
-                      in (MAbs (s, T, M, V x, m'), accum |>> pop_bound) end))
-         | @{const Not} $ t1 => do_connect imp_triple t1 @{const False} accum
-         | @{const conj} $ t1 $ t2 => do_connect conj_triple t1 t2 accum
-         | @{const disj} $ t1 $ t2 => do_connect disj_triple t1 t2 accum
-         | @{const implies} $ t1 $ t2 => do_connect imp_triple t1 t2 accum
+                      in (MFun (M, V x, M'), accum |>> pop_bound) end))
+         | @{const Not} $ t1 => do_connect imp_spec t1 @{const False} accum
+         | @{const conj} $ t1 $ t2 => do_connect conj_spec t1 t2 accum
+         | @{const disj} $ t1 $ t2 => do_connect disj_spec t1 t2 accum
+         | @{const implies} $ t1 $ t2 => do_connect imp_spec t1 t2 accum
          | Const (@{const_name Let}, _) $ t1 $ t2 =>
            do_term (betapply (t2, t1)) accum
          | t1 $ t2 =>
@@ -1028,121 +964,106 @@
              val frame2b =
                frame1b |> map (apsnd (fn _ => V (Unsynchronized.inc max_fresh)))
              val frame2 = frame2a @ frame2b
-             val (m1, accum) = accum |>> set_frame frame1a |> do_term t1
-             val (m2, accum) = accum |>> set_frame frame2 |> do_term t2
+             val (M1, accum) = accum |>> set_frame frame1a |> do_term t1
+             val (M2, accum) = accum |>> set_frame frame2 |> do_term t2
            in
              let
-               val (M11, aa, _) = mtype_of_mterm m1 |> dest_MFun
-               val M2 = mtype_of_mterm m2
+               val (M11, aa, M12) = M1 |> dest_MFun
              in
-               (MApp (m1, m2),
-                accum |>> set_frame frame
-                      ||> add_is_sub_mtype M2 M11
-                      ||> add_app aa frame1b frame2b)
+               (M12, accum |>> set_frame frame
+                           ||> add_is_sub_mtype M2 M11
+                           ||> add_app aa frame1b frame2b)
              end
            end)
-        |> tap (fn (m, (gamma, _)) =>
+        |> tap (fn (M, (gamma, _)) =>
                    trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
                                        " \<turnstile> " ^
-                                       string_for_mterm ctxt m))
+                                       Syntax.string_of_term ctxt t ^ " : " ^
+                                       string_for_mtype M))
   in do_term end
 
 fun force_gen_funs 0 _ = I
   | force_gen_funs n (M as MFun (M1, _, M2)) =
     add_mtypes_equal M (MFun (M1, A Gen, M2)) #> force_gen_funs (n - 1) M2
   | force_gen_funs _ M = raise MTYPE ("Nitpick_Mono.force_gen_funs", [M], [])
-fun consider_general_equals mdata def (x as (_, T)) t1 t2 accum =
+fun consider_general_equals mdata def 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 (M1, accum) = consider_term mdata t1 accum
+    val (M2, accum) = consider_term mdata t2 accum
     val accum = accum ||> add_mtypes_equal M1 M2
-    val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
-    val m = MApp (MApp (MRaw (Const x,
-                           MFun (M1, A Gen, MFun (M2, A Gen, body_M))), m1), m2)
   in
-    (m, (if def then
-           let val (head_m, arg_ms) = strip_mcomb m1 in
-             accum ||> force_gen_funs (length arg_ms) (mtype_of_mterm head_m)
-           end
-         else
-           accum))
+    if def then
+      let
+        val (head1, args1) = strip_comb t1
+        val (head_M1, accum) = consider_term mdata head1 accum
+      in accum ||> force_gen_funs (length args1) head_M1 end
+    else
+      accum
   end
 
 fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, max_fresh,
                                         ...}) =
   let
     val mtype_for = fresh_mtype_for_type mdata false
-    val do_term = consider_term mdata
+    val do_term = snd oo consider_term mdata
     fun do_formula sn t (accum as (gamma, _)) =
       let
-        fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
+        fun do_quantifier quant_s abs_T body_t =
           let
             val abs_M = mtype_for abs_T
             val x = Unsynchronized.inc max_fresh
             val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
             fun ann () = if quant_s = @{const_name Ex} then Fls else Tru
-            val (body_m, accum) =
-              accum ||> side_cond
-                        ? add_mtype_is_complete [(x, (Plus, ann ()))] abs_M
-                    |>> push_bound (V x) abs_T abs_M |> do_formula sn body_t
-            val body_M = mtype_of_mterm body_m
           in
-            (MApp (MRaw (Const quant_x,
-                         MFun (MFun (abs_M, A Gen, body_M), A Gen, body_M)),
-                   MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
-             accum |>> pop_bound)
+            accum ||> side_cond
+                      ? add_mtype_is_complete [(x, (Plus, ann ()))] abs_M
+                  |>> push_bound (V x) abs_T abs_M
+                  |> do_formula sn body_t
+                  |>> pop_bound
           end
-        fun do_connect triple neg1 t1 t2 =
-          consider_connective mdata triple
+        fun do_connect spec neg1 t1 t2 =
+          consider_connective mdata spec
               (do_formula (sn |> neg1 ? negate_sign) t1) (do_formula sn t2)
-        fun do_equals x t1 t2 =
+        fun do_equals t1 t2 =
           case sn of
             Plus => do_term t accum
-          | Minus => consider_general_equals mdata false x t1 t2 accum
+          | Minus => consider_general_equals mdata false t1 t2 accum
       in
         trace_msg (fn () => "  " ^ string_for_mcontext ctxt t gamma ^
                             " \<turnstile> " ^ Syntax.string_of_term ctxt t ^
                             " : o\<^sup>" ^ string_for_sign sn ^ "?");
         case t of
-          Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
-          do_quantifier x s1 T1 t1
-        | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
-        | @{const Trueprop} $ t1 =>
-          let val (m1, accum) = do_formula sn t1 accum in
-            (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)), m1),
-             accum)
-          end
-        | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
-          do_quantifier x s1 T1 t1
-        | Const (x0 as (@{const_name Ex}, T0)) $ (t1 as Abs (s1, T1, t1')) =>
+          Const (s as @{const_name all}, _) $ Abs (_, T1, t1) =>
+          do_quantifier s T1 t1
+        | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2
+        | @{const Trueprop} $ t1 => do_formula sn t1 accum
+        | Const (s as @{const_name All}, _) $ Abs (_, T1, t1) =>
+          do_quantifier s T1 t1
+        | Const (s as @{const_name Ex}, T0) $ (t1 as Abs (_, T1, t1')) =>
           (case sn of
-             Plus => do_quantifier x0 s1 T1 t1'
+             Plus => do_quantifier s T1 t1'
            | Minus =>
-             (* FIXME: Move elsewhere *)
+             (* FIXME: Needed? *)
              do_term (@{const Not}
                       $ (HOLogic.eq_const (domain_type T0) $ t1
                          $ Abs (Name.uu, T1, @{const False}))) accum)
-        | Const (x as (@{const_name HOL.eq}, _)) $ t1 $ t2 => do_equals x t1 t2
+        | Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_equals t1 t2
         | Const (@{const_name Let}, _) $ t1 $ t2 =>
           do_formula sn (betapply (t2, t1)) accum
         | @{const Pure.conjunction} $ t1 $ t2 =>
-          do_connect meta_conj_triple false t1 t2 accum
-        | @{const "==>"} $ t1 $ t2 =>
-          do_connect meta_imp_triple true t1 t2 accum
-        | @{const Not} $ t1 =>
-          do_connect imp_triple true t1 @{const False} accum
-        | @{const conj} $ t1 $ t2 => do_connect conj_triple false t1 t2 accum
-        | @{const disj} $ t1 $ t2 => do_connect disj_triple false t1 t2 accum
-        | @{const implies} $ t1 $ t2 => do_connect imp_triple true t1 t2 accum
+          do_connect meta_conj_spec false t1 t2 accum
+        | @{const "==>"} $ t1 $ t2 => do_connect meta_imp_spec true t1 t2 accum
+        | @{const Not} $ t1 => do_connect imp_spec true t1 @{const False} accum
+        | @{const conj} $ t1 $ t2 => do_connect conj_spec false t1 t2 accum
+        | @{const disj} $ t1 $ t2 => do_connect disj_spec false t1 t2 accum
+        | @{const implies} $ t1 $ t2 => do_connect imp_spec true t1 t2 accum
         | _ => do_term t accum
       end
-      |> tap (fn (m, (gamma, _)) =>
+      |> tap (fn (gamma, _) =>
                  trace_msg (fn () => string_for_mcontext ctxt t gamma ^
                                      " \<turnstile> " ^
-                                     string_for_mterm ctxt m ^ " : o\<^sup>" ^
-                                     string_for_sign sn))
+                                     Syntax.string_of_term ctxt t ^
+                                     " : o\<^sup>" ^ string_for_sign sn))
   in do_formula end
 
 (* The harmless axiom optimization below is somewhat too aggressive in the face
@@ -1151,72 +1072,44 @@
   [@{const_name ord_class.less}, @{const_name ord_class.less_eq}]
 val bounteous_consts = [@{const_name bisim}]
 
-fun is_harmless_axiom ({no_harmless = true, ...} : mdata) _ = false
-  | is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
+fun is_harmless_axiom {hol_ctxt = {thy, stds, ...}, ...} t =
     Term.add_consts t []
     |> filter_out (is_built_in_const thy stds)
     |> (forall (member (op =) harmless_consts o original_name o fst) orf
         exists (member (op =) bounteous_consts o fst))
 
 fun consider_nondefinitional_axiom mdata t =
-  if is_harmless_axiom mdata t then pair (MRaw (t, dummy_M))
+  if is_harmless_axiom mdata t then I
   else consider_general_formula mdata Plus t
 
 fun consider_definitional_axiom (mdata as {hol_ctxt = {ctxt, ...}, ...}) t =
   if not (is_constr_pattern_formula ctxt t) then
     consider_nondefinitional_axiom mdata t
   else if is_harmless_axiom mdata t then
-    pair (MRaw (t, dummy_M))
+    I
   else
     let
       val mtype_for = fresh_mtype_for_type mdata false
-      val do_term = consider_term mdata
-      fun do_all quant_t abs_s abs_T body_t accum =
-        let
-          val abs_M = mtype_for abs_T
-          val (body_m, accum) =
-            accum |>> push_bound (A Gen) abs_T abs_M |> do_formula body_t
-          val body_M = mtype_of_mterm body_m
-        in
-          (MApp (MRaw (quant_t, MFun (MFun (abs_M, A Gen, body_M), A Gen,
-                       body_M)),
-                 MAbs (abs_s, abs_T, abs_M, A Gen, body_m)),
-           accum |>> pop_bound)
-        end
-      and do_conjunction t0 t1 t2 accum =
-        let
-          val (m1, accum) = do_formula t1 accum
-          val (m2, accum) = do_formula t2 accum
-        in
-          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
-        end
-      and do_implies t0 t1 t2 accum =
-        let
-          val (m1, accum) = do_term t1 accum
-          val (m2, accum) = do_formula t2 accum
-        in
-          (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
-        end
+      val do_term = snd oo consider_term mdata
+      fun do_all abs_T body_t accum =
+        accum |>> push_bound (A Gen) abs_T (mtype_for abs_T)
+              |> do_formula body_t
+              |>> pop_bound
+      and do_implies t1 t2 = do_term t1 #> do_formula t2
       and do_formula t accum =
         case t of
-          (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
-          do_all t0 s1 T1 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 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 HOL.eq}, _)) $ t1 $ t2 =>
-          consider_general_equals mdata true x t1 t2 accum
-        | (t0 as @{const conj}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
-        | (t0 as @{const implies}) $ t1 $ t2 => do_implies t0 t1 t2 accum
+          Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
+        | @{const Trueprop} $ t1 => do_formula t1 accum
+        | Const (@{const_name "=="}, _) $ t1 $ t2 =>
+          consider_general_equals mdata true t1 t2 accum
+        | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum
+        | @{const Pure.conjunction} $ t1 $ t2 =>
+          fold (do_formula) [t1, t2] accum
+        | Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
+        | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
+          consider_general_equals mdata true t1 t2 accum
+        | @{const conj} $ t1 $ t2 => fold (do_formula) [t1, t2] accum
+        | @{const implies} $ t1 $ t2 => do_implies t1 t2 accum
         | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
                            \do_formula", [t])
     in do_formula t end
@@ -1230,143 +1123,26 @@
       map (fn (x, M) => string_for_mtype_of_term ctxt asgs (Const x) M) consts
       |> cat_lines)
 
-fun amass f t (ms, accum) =
-  let val (m, accum) = f t accum in (m :: ms, accum) end
-
-fun infer which no_harmless (hol_ctxt as {ctxt, tac_timeout, ...}) binarize
-          alpha_T (nondef_ts, def_ts) =
+fun formulas_monotonic (hol_ctxt as {ctxt, tac_timeout, ...}) binarize alpha_T
+                       (nondef_ts, def_ts) =
   let
-    val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
+    val _ = trace_msg (fn () => "****** Monotonicity analysis: " ^
                                 string_for_mtype MAlpha ^ " is " ^
                                 Syntax.string_of_typ ctxt alpha_T)
-    val mdata as {max_fresh, constr_mcache, ...} =
-      initial_mdata hol_ctxt binarize no_harmless alpha_T
-    val accum = (initial_gamma, ([], []))
-    val (nondef_ms, accum) =
-      ([], 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 (amass (consider_definitional_axiom mdata)) def_ts
+    val mdata as {max_fresh, ...} = initial_mdata hol_ctxt binarize alpha_T
+    val (gamma, cset) =
+      (initial_gamma, ([], []))
+      |> consider_general_formula mdata Plus (hd nondef_ts)
+      |> fold (consider_nondefinitional_axiom mdata) (tl nondef_ts)
+      |> fold (consider_definitional_axiom mdata) def_ts
   in
     case solve tac_timeout (!max_fresh) cset of
-      SOME asgs => (print_mcontext ctxt asgs gamma;
-                    SOME (asgs, (nondef_ms, def_ms), !constr_mcache))
-    | _ => NONE
+      SOME asgs => (print_mcontext ctxt asgs gamma; true)
+    | _ => false
   end
-  handle UNSOLVABLE () => NONE
+  handle UNSOLVABLE () => false
        | 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))
-
-val formulas_monotonic = is_some oooo infer "Monotonicity" false
-
-fun fin_fun_constr T1 T2 =
-  (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
-
-fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize
-                  finitizes alpha_T tsp =
-  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
-    SOME (asgs, msp, constr_mtypes) =>
-    if forall (curry (op =) Gen o snd) asgs then
-      tsp
-    else
-      let
-        fun should_finitize T aa =
-          case triple_lookup (type_match thy) finitizes T of
-            SOME (SOME false) => false
-          | _ => resolve_annotation_atom asgs aa = A Fls
-        fun type_from_mtype T M =
-          case (M, T) of
-            (MAlpha, _) => T
-          | (MFun (M1, aa, M2), Type (@{type_name fun}, Ts)) =>
-            Type (if should_finitize T aa then @{type_name fin_fun}
-                  else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
-          | (MPair (M1, M2), Type (@{type_name prod}, Ts)) =>
-            Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2])
-          | (MType _, _) => T
-          | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
-                              [M], [T])
-        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)
-        fun term_from_mterm new_Ts old_Ts m =
-          case m of
-            MRaw (t, M) =>
-            let
-              val T = fastype_of1 (old_Ts, t)
-              val T' = type_from_mtype T M
-            in
-              case t of
-                Const (x as (s, _)) =>
-                if s = @{const_name finite} then
-                  case domain_type T' of
-                    set_T' as Type (@{type_name fin_fun}, _) =>
-                    Abs (Name.uu, set_T', @{const True})
-                  | _ => Const (s, T')
-                else if s = @{const_name "=="} orelse
-                        s = @{const_name HOL.eq} then
-                  let
-                    val T =
-                      case T' of
-                        Type (_, [T1, Type (_, [T2, T3])]) =>
-                        T1 --> T2 --> T3
-                      | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\
-                                         \term_from_mterm", [T, T'], [])
-                  in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end
-                else if is_built_in_const thy stds x then
-                  coerce_term hol_ctxt new_Ts T' T t
-                else if is_constr ctxt 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
-          | MApp (m1, m2) =>
-            let
-              val (t1, t2) = pairself (term_from_mterm new_Ts old_Ts) (m1, m2)
-              val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
-              val (t1', T2') =
-                case T1 of
-                  Type (s, [T11, T12]) =>
-                  (if s = @{type_name fin_fun} then
-                     select_nth_constr_arg ctxt 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 new_Ts T2' T2 t2) end
-          | MAbs (s, old_T, M, aa, m') =>
-            let
-              val new_T = type_from_mtype old_T M
-              val t' = term_from_mterm (new_T :: new_Ts) (old_T :: old_Ts) m'
-              val T' = fastype_of1 (new_T :: new_Ts, t')
-            in
-              Abs (s, new_T, t')
-              |> should_finitize (new_T --> T') aa
-                 ? construct_value ctxt stds (fin_fun_constr new_T T') o single
-            end
-      in
-        Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
-        pairself (map (term_from_mterm [] [])) msp
-      end
-  | NONE => tsp
 
 end;
diff -r 1c0eefa8d02a -r d6f45159ae84 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 11:50:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 12:10:13 2010 +0100
@@ -55,8 +55,6 @@
     Eq |
     Triad |
     Composition |
-    Product |
-    Image |
     Apply |
     Lambda
 
@@ -170,8 +168,6 @@
   Eq |
   Triad |
   Composition |
-  Product |
-  Image |
   Apply |
   Lambda
 
@@ -235,8 +231,6 @@
   | string_for_op2 Eq = "Eq"
   | string_for_op2 Triad = "Triad"
   | string_for_op2 Composition = "Composition"
-  | string_for_op2 Product = "Product"
-  | string_for_op2 Image = "Image"
   | string_for_op2 Apply = "Apply"
   | string_for_op2 Lambda = "Lambda"
 
@@ -528,10 +522,6 @@
           Op1 (Closure, range_type T, Any, sub t1)
         | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
-        | (Const (@{const_name Sigma}, T), [t1, Abs (s, T', t2')]) =>
-          Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2')
-        | (Const (@{const_name image}, T), [t1, t2]) =>
-          Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
         | (Const (x as (s as @{const_name Suc}, T)), []) =>
           if is_built_in_const thy stds x then Cst (Suc, T, Any)
           else if is_constr ctxt stds x then do_construct x []
@@ -941,46 +931,6 @@
               Cst (False, T, Formula Pos)
               |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u))
           end
-        | Op2 (Image, T, _, u1, u2) =>
-          let
-            val u1' = sub u1
-            val u2' = sub u2
-          in
-            (case (rep_of u1', rep_of u2') of
-               (Func (R11, R12), Func (R21, Formula Neut)) =>
-               if R21 = R11 andalso is_lone_rep R12 then
-                 let
-                   val R =
-                     best_non_opt_set_rep_for_type scope T
-                     |> exists (is_opt_rep o rep_of) [u1', u2'] ? opt_rep ofs T
-                 in s_op2 Image T R u1' u2' end
-               else
-                 raise SAME ()
-             | _ => raise SAME ())
-            handle SAME () =>
-                   let
-                     val T1 = type_of u1
-                     val dom_T = domain_type T1
-                     val ran_T = range_type T1
-                     val x_u = BoundName (~1, dom_T, Any, "image.x")
-                     val y_u = BoundName (~2, ran_T, Any, "image.y")
-                   in
-                     Op2 (Lambda, T, Any, y_u,
-                          Op2 (Exist, bool_T, Any, x_u,
-                               Op2 (And, bool_T, Any,
-                                    case u2 of
-                                      Op2 (Lambda, _, _, u21, u22) =>
-                                      if num_occurrences_in_nut u21 u22 = 0 then
-                                        u22
-                                      else
-                                        Op2 (Apply, bool_T, Any, u2, x_u)
-                                    | _ => Op2 (Apply, bool_T, Any, u2, x_u),
-
-                                    Op2 (Eq, bool_T, Any, y_u,
-                                         Op2 (Apply, ran_T, Any, u1, x_u)))))
-                     |> sub
-                   end
-          end
         | Op2 (Apply, T, _, u1, u2) =>
           let
             val u1 = sub u1
diff -r 1c0eefa8d02a -r d6f45159ae84 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 07 11:50:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 07 12:10:13 2010 +0100
@@ -9,8 +9,7 @@
 sig
   type hol_context = Nitpick_HOL.hol_context
   val preprocess_formulas :
-    hol_context -> (typ option * bool option) list
-    -> (typ option * bool option) list -> term list -> term
+    hol_context -> term list -> term
     -> term list * term list * bool * bool * bool
 end;
 
@@ -1245,32 +1244,13 @@
              | _ => t
   in aux "" [] [] end
 
-(** Inference of finite functions **)
-
-fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
-                               (nondef_ts, def_ts) =
-  if forall (curry (op =) (SOME false) o snd) finitizes then
-    (nondef_ts, def_ts)
-  else
-    let
-      val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
-               |> filter_out (fn Type (@{type_name fun_box}, _) => true
-                               | @{typ signed_bit} => true
-                               | @{typ unsigned_bit} => 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 **)
 
 val max_skolem_depth = 3
 
 fun preprocess_formulas
         (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
-                      ...}) finitizes monos assm_ts neg_t =
+                      ...}) assm_ts neg_t =
   let
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
       neg_t |> unfold_defs_in_term hol_ctxt
@@ -1307,9 +1287,6 @@
       #> 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 1c0eefa8d02a -r d6f45159ae84 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Dec 07 11:50:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Dec 07 12:10:13 2010 +0100
@@ -112,8 +112,6 @@
 
 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 (@{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 prod}, Ts)) =
     forall (is_complete_type dtypes facto) Ts
   | is_complete_type dtypes facto T =
@@ -122,8 +120,6 @@
     handle Option.Option => true
 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 (@{type_name fin_fun}, [_, T2])) =
-    is_concrete_type dtypes facto T2
   | is_concrete_type dtypes facto (Type (@{type_name prod}, Ts)) =
     forall (is_concrete_type dtypes facto) Ts
   | is_concrete_type dtypes facto T =