1.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 17:59:22 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 18:29:00 2009 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4      the formula to falsify
     1.5    * Added support for codatatype view of datatypes
     1.6    * Fixed soundness bugs related to sets, sets of sets, (co)inductive
     1.7 -    predicates, and typedefs
     1.8 +    predicates, typedefs, and "finite"
     1.9    * Fixed monotonicity check
    1.10    * Fixed error when processing definitions
    1.11    * Fixed error in "star_linear_preds" optimization

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 23 17:59:22 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 23 18:29:00 2009 +0100
     2.3 @@ -251,7 +251,7 @@
     2.4      val intro_table = inductive_intro_table ctxt def_table
     2.5      val ground_thm_table = ground_theorem_table thy
     2.6      val ersatz_table = ersatz_table thy
     2.7 -    val (ext_ctxt as {skolems, special_funs, wf_cache, ...}) =
     2.8 +    val (ext_ctxt as {wf_cache, ...}) =
     2.9        {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
    2.10         user_axioms = user_axioms, debug = debug, wfs = wfs,
    2.11         destroy_constrs = destroy_constrs, specialize = specialize,
    2.12 @@ -296,11 +296,9 @@
    2.13              handle TYPE (_, Ts, ts) =>
    2.14                     raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
    2.15  
    2.16 -    val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t
    2.17 -    val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq)
    2.18 -                     def_ts
    2.19 -    val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq)
    2.20 -                        nondef_ts
    2.21 +    val core_u = nut_from_term ext_ctxt Eq core_t
    2.22 +    val def_us = map (nut_from_term ext_ctxt DefEq) def_ts
    2.23 +    val nondef_us = map (nut_from_term ext_ctxt Eq) nondef_ts
    2.24      val (free_names, const_names) =
    2.25        fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
    2.26      val (sel_names, nonsel_names) =

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 17:59:22 2009 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Nov 23 18:29:00 2009 +0100
     3.3 @@ -1496,14 +1496,7 @@
     3.4          let
     3.5            val (const, ts) =
     3.6              if is_built_in_const fast_descrs x then
     3.7 -              if s = @{const_name finite} then
     3.8 -                if is_finite_type ext_ctxt (domain_type T) then
     3.9 -                  (Abs ("A", domain_type T, @{const True}), ts)
    3.10 -                else case ts of
    3.11 -                  [Const (@{const_name top}, _)] => (@{const False}, [])
    3.12 -                | _ => (Const x, ts)
    3.13 -              else
    3.14 -                (Const x, ts)
    3.15 +              (Const x, ts)
    3.16              else case AList.lookup (op =) case_names s of
    3.17                SOME n =>
    3.18                let

     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Nov 23 17:59:22 2009 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Nov 23 18:29:00 2009 +0100
     4.3 @@ -106,7 +106,7 @@
     4.4    val name_ord : (nut * nut) -> order
     4.5    val the_name : 'a NameTable.table -> nut -> 'a
     4.6    val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
     4.7 -  val nut_from_term : theory -> bool -> special_fun list -> op2 -> term -> nut
     4.8 +  val nut_from_term : extended_context -> op2 -> term -> nut
     4.9    val choose_reps_for_free_vars :
    4.10      scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
    4.11    val choose_reps_for_consts :
    4.12 @@ -464,8 +464,8 @@
    4.13  fun factorize (z as (Type ("*", _), _)) = maps factorize [mk_fst z, mk_snd z]
    4.14    | factorize z = [z]
    4.15  
    4.16 -(* theory -> bool -> special_fun list -> op2 -> term -> nut *)
    4.17 -fun nut_from_term thy fast_descrs special_funs eq =
    4.18 +(* extended_context -> op2 -> term -> nut *)
    4.19 +fun nut_from_term (ext_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
    4.20    let
    4.21      (* string list -> typ list -> term -> nut *)
    4.22      fun aux eq ss Ts t =
    4.23 @@ -596,7 +596,11 @@
    4.24            Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
    4.25          | (Const (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
    4.26          | (Const (@{const_name finite}, T), [t1]) =>
    4.27 -          Op1 (Finite, bool_T, Any, sub t1)
    4.28 +          (if is_finite_type ext_ctxt (domain_type T) then
    4.29 +             Cst (True, bool_T, Any)
    4.30 +           else case t1 of
    4.31 +             Const (@{const_name top}, _) => Cst (False, bool_T, Any)
    4.32 +           | _ => Op1 (Finite, bool_T, Any, sub t1))
    4.33          | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
    4.34          | (Const (@{const_name zero_nat_inst.zero_nat}, T), []) =>
    4.35            Cst (Num 0, T, Any)
    4.36 @@ -678,7 +682,7 @@
    4.37               | NONE => if null ts then ConstName (s, T, Any)
    4.38                         else do_apply t0 ts)
    4.39          | (Free (s, T), []) => FreeName (s, T, Any)
    4.40 -        | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term", [t])
    4.41 +        | (Var _, []) => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
    4.42          | (Bound j, []) =>
    4.43            BoundName (length Ts - j - 1, nth Ts j, Any, nth ss j)
    4.44          | (Abs (s, T, t1), []) =>