# HG changeset patch
# User blanchet
# Date 1266836253 -3600
# Node ID 54ab4921f826386eb127226674dac672e61028e8
# Parent  4f6760122b2aba1978f528fb3bd914abeaf67ebc
fixed a few bugs in Nitpick and removed unreferenced variables

diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -465,7 +465,7 @@
   | arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1
   | arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2
   | arity_of_rel_expr (IfNo (r1, _)) = arity_of_rel_expr r1
-  | arity_of_rel_expr (Project (r, is)) = length is
+  | arity_of_rel_expr (Project (_, is)) = length is
   | arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2 - 2
   | arity_of_rel_expr (Closure _) = 2
   | arity_of_rel_expr (ReflexiveClosure _) = 2
@@ -590,8 +590,8 @@
         (case tuple_set of
            TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1)
          | TupleDifference (ts1, ts2) =>
-           sub ts1 prec ^ " - " ^ sub ts1 (prec + 1)
-         | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts1 prec
+           sub ts1 prec ^ " - " ^ sub ts2 (prec + 1)
+         | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec
          | TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec
          | TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]"
          | TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}"
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -128,7 +128,7 @@
          All (decls_for SRep card Ts T, to_F (T :: Ts) t')
        | (t0 as Const (@{const_name All}, _)) $ t1 =>
          to_F Ts (t0 $ eta_expand Ts t1 1)
-       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
+       | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
          Exist (decls_for SRep card Ts T, to_F (T :: Ts) t')
        | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
          to_F Ts (t0 $ eta_expand Ts t1 1)
@@ -234,7 +234,7 @@
        | Free (x as (_, T)) =>
          Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
        | Term.Var _ => raise NOT_SUPPORTED "schematic variables"
-       | Bound j => raise SAME ()
+       | Bound _ => raise SAME ()
        | Abs (_, T, t') =>
          (case fastype_of1 (T :: Ts, t') of
             @{typ bool} => Comprehension (decls_for SRep card Ts T,
@@ -251,11 +251,8 @@
             let val T2 = fastype_of1 (Ts, t2) in
               case arity_of SRep card T2 of
                 1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
-              | n =>
-                let
-                  val arity2 = arity_of SRep card T2
-                  val res_arity = arity_of RRep card T
-                in
+              | arity2 =>
+                let val res_arity = arity_of RRep card T in
                   Project (Intersect
                       (Product (to_S_rep Ts t2,
                                 atom_schema_of RRep card T
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -201,13 +201,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, blocking, 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, 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 *)
@@ -227,7 +227,6 @@
     (* (unit -> string) -> unit *)
     val print_m = pprint_m o K o plazy
     val print_v = pprint_v o K o plazy
-    val print_d = pprint_d o K o plazy
 
     (* unit -> unit *)
     fun check_deadline () =
@@ -489,9 +488,9 @@
         val core_u = rename_vars_in_nut pool rel_table core_u
         val def_us = map (rename_vars_in_nut pool rel_table) def_us
         val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
-        val core_f = kodkod_formula_from_nut bits ofs kk core_u
-        val def_fs = map (kodkod_formula_from_nut bits ofs kk) def_us
-        val nondef_fs = map (kodkod_formula_from_nut bits ofs kk) nondef_us
+        val core_f = kodkod_formula_from_nut ofs kk core_u
+        val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
+        val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
         val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
         val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
                       PrintMode.setmp [] multiline_string_for_scope scope
@@ -535,9 +534,8 @@
       in
         SOME ({comment = comment, settings = settings, univ_card = univ_card,
                tuple_assigns = [], bounds = bounds,
-               int_bounds =
-                   if bits = 0 then sequential_int_bounds univ_card
-                   else pow_of_two_int_bounds bits main_j0 univ_card,
+               int_bounds = if bits = 0 then sequential_int_bounds univ_card
+                            else pow_of_two_int_bounds bits main_j0,
                expr_assigns = [], formula = formula},
               {free_names = free_names, sel_names = sel_names,
                nonsel_names = nonsel_names, rel_table = rel_table,
@@ -562,17 +560,13 @@
                                                     else "genuine") ^
                                    " component of scope."));
                 NONE)
-           | TOO_SMALL (loc, msg) =>
+           | TOO_SMALL (_, msg) =>
              (print_v (fn () => ("Limit reached: " ^ msg ^
                                  ". Skipping " ^ (if unsound then "potential"
                                                   else "genuine") ^
                                  " component of scope."));
               NONE)
 
-    (* int -> (''a * int list list) list -> ''a -> KK.tuple_set *)
-    fun tuple_set_for_rel univ_card =
-      KK.TupleSet o map (kk_tuple debug univ_card) o the oo AList.lookup (op =)
-
     val das_wort_model =
       (if falsify then "counterexample" else "model")
       |> not standard ? prefix "nonstandard "
@@ -809,8 +803,7 @@
             ()
         (* scope * bool -> rich_problem list * bool
            -> rich_problem list * bool *)
-        fun add_problem_for_scope (scope as {datatypes, ...}, unsound)
-                                  (problems, donno) =
+        fun add_problem_for_scope (scope, unsound) (problems, donno) =
           (check_deadline ();
            case problem_for_scope unsound scope of
              SOME problem =>
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -65,6 +65,7 @@
   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 string_for_type : Proof.context -> typ -> string
   val prefix_name : string -> string -> string
   val shortest_name : string -> string
@@ -81,6 +82,7 @@
   val is_lfp_iterator_type : typ -> bool
   val is_gfp_iterator_type : typ -> bool
   val is_fp_iterator_type : typ -> bool
+  val is_iterator_type : typ -> bool
   val is_boolean_type : typ -> bool
   val is_integer_type : typ -> bool
   val is_bit_type : typ -> bool
@@ -261,7 +263,6 @@
 val set_prefix = nitpick_prefix ^ "set" ^ name_sep
 val lfp_iterator_prefix = nitpick_prefix ^ "lfpit" ^ name_sep
 val gfp_iterator_prefix = nitpick_prefix ^ "gfpit" ^ name_sep
-val nwf_prefix = nitpick_prefix ^ "nwf" ^ name_sep
 val unrolled_prefix = nitpick_prefix ^ "unroll" ^ name_sep
 val base_prefix = nitpick_prefix ^ "base" ^ name_sep
 val step_prefix = nitpick_prefix ^ "step" ^ name_sep
@@ -306,7 +307,7 @@
     if t0 = conn_t then strip_connective t0 t2 @ strip_connective t0 t1 else [t]
   | strip_connective _ t = [t]
 (* term -> term list * term *)
-fun strip_any_connective (t as (t0 $ t1 $ t2)) =
+fun strip_any_connective (t as (t0 $ _ $ _)) =
     if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
       (strip_connective t0 t, t0)
     else
@@ -389,7 +390,6 @@
 (* typ -> typ *)
 fun unarize_type @{typ "unsigned_bit word"} = nat_T
   | unarize_type @{typ "signed_bit word"} = int_T
-  | unarize_type @{typ bisim_iterator} = nat_T
   | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
   | unarize_type T = T
 fun unarize_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
@@ -398,10 +398,14 @@
     Type ("*", map unarize_and_unbox_type Ts)
   | unarize_and_unbox_type @{typ "unsigned_bit word"} = nat_T
   | unarize_and_unbox_type @{typ "signed_bit word"} = int_T
-  | unarize_and_unbox_type @{typ bisim_iterator} = nat_T
   | unarize_and_unbox_type (Type (s, Ts as _ :: _)) =
     Type (s, map unarize_and_unbox_type Ts)
   | unarize_and_unbox_type T = T
+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
+
 (* Proof.context -> typ -> string *)
 fun string_for_type ctxt = Syntax.string_of_typ ctxt o unarize_and_unbox_type
 
@@ -436,7 +440,7 @@
 fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
   | term_match thy (Free (s1, T1), Free (s2, T2)) =
     const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
-  | term_match thy (t1, t2) = t1 aconv t2
+  | term_match _ (t1, t2) = t1 aconv t2
 
 (* typ -> bool *)
 fun is_TFree (TFree _) = true
@@ -455,14 +459,14 @@
 fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
   | is_gfp_iterator_type _ = false
 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
+fun is_iterator_type T =
+  (T = @{typ bisim_iterator} orelse is_fp_iterator_type T)
 fun is_boolean_type T = (T = prop_T orelse T = bool_T)
 fun is_integer_type T = (T = nat_T orelse T = int_T)
 fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
 fun is_word_type (Type (@{type_name word}, _)) = true
   | is_word_type _ = false
-fun is_integer_like_type T =
-  is_fp_iterator_type T orelse is_integer_type T orelse is_word_type T orelse
-  T = @{typ bisim_iterator}
+val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type
 val is_record_type = not o null o Record.dest_recTs
 (* theory -> typ -> bool *)
 fun is_frac_type thy (Type (s, [])) =
@@ -596,7 +600,7 @@
 fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
   | is_quot_type _ (Type ("FSet.fset", _)) = true
   | is_quot_type _ _ = false
-fun is_codatatype thy (T as Type (s, _)) =
+fun is_codatatype thy (Type (s, _)) =
     not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
                |> Option.map snd |> these))
   | is_codatatype _ _ = false
@@ -630,7 +634,7 @@
   end
   handle TYPE _ => []
 (* styp -> bool *)
-fun is_record_constr (x as (s, T)) =
+fun is_record_constr (s, T) =
   String.isSuffix Record.extN s andalso
   let val dataT = body_type T in
     is_record_type dataT andalso
@@ -706,7 +710,7 @@
   member (op =) [@{const_name FunBox}, @{const_name PairBox},
                  @{const_name Quot}, @{const_name Zero_Rep},
                  @{const_name Suc_Rep}] s orelse
-  let val (x as (s, T)) = (s, unarize_and_unbox_type T) in
+  let val (x as (_, T)) = (s, unarize_and_unbox_type T) in
     Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
     (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
     is_coconstr thy x
@@ -747,7 +751,7 @@
             (map (box_type hol_ctxt InPair) Ts))
   | _ => false
 (* hol_context -> boxability -> string * typ list -> string *)
-and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
+and should_box_type (hol_ctxt as {thy, boxes, ...}) boxy z =
   case triple_lookup (type_match thy) boxes (Type z) of
     SOME (SOME box_me) => box_me
   | _ => is_boxing_worth_it hol_ctxt boxy (Type z)
@@ -934,9 +938,9 @@
       Abs (Name.uu, dataT, @{const True})
   end
 (* hol_context -> styp -> term -> term *)
-fun discriminate_value (hol_ctxt as {thy, ...}) (x as (_, T)) t =
-  case strip_comb t of
-    (Const x', args) =>
+fun discriminate_value (hol_ctxt as {thy, ...}) x t =
+  case head_of t of
+    Const x' =>
     if x = x' then @{const True}
     else if is_constr_like thy x' then @{const False}
     else betapply (discr_term_for_constr hol_ctxt x, t)
@@ -979,7 +983,7 @@
   | construct_value thy stds (x as (s, _)) args =
     let val args = map Envir.eta_contract args in
       case hd args of
-        Const (x' as (s', _)) $ t =>
+        Const (s', _) $ t =>
         if is_sel_like_and_no_discr s' andalso
            constr_name_for_sel_like s' = s andalso
            forall (fn (n, t') =>
@@ -1063,9 +1067,8 @@
           | constrs =>
             let
               val constr_cards =
-                datatype_constrs hol_ctxt T
-                |> map (Integer.prod o map (aux (T :: avoid)) o binder_types
-                        o snd)
+                map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
+                    constrs
             in
               if exists (curry (op =) 0) constr_cards then 0
               else Integer.sum constr_cards
@@ -1199,10 +1202,15 @@
                  (s, unarize_type T) of
           SOME n => SOME n
         | NONE =>
-          if is_fun_type T andalso is_set_type (domain_type T) then
-            AList.lookup (op =) built_in_set_consts s
-          else
-            NONE
+          case s of
+            @{const_name zero_class.zero} =>
+            if is_iterator_type T then SOME 0 else NONE
+          | @{const_name Suc} =>
+            if is_iterator_type (domain_type T) then SOME 0 else NONE
+          | _ => if is_fun_type T andalso is_set_type (domain_type T) then
+                   AList.lookup (op =) built_in_set_consts s
+                 else
+                   NONE
     end
 (* theory -> (typ option * bool) list -> bool -> styp -> bool *)
 val is_built_in_const = is_some oooo arity_of_built_in_const
@@ -1233,12 +1241,12 @@
     |> map_filter (try (Refute.specialize_type thy x))
     |> filter (curry (op =) (Const x) o term_under_def)
 
-(* theory -> term -> term option *)
-fun normalized_rhs_of thy t =
+(* term -> term option *)
+fun normalized_rhs_of t =
   let
     (* term option -> term option *)
     fun aux (v as Var _) (SOME t) = SOME (lambda v t)
-      | aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t)
+      | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t)
       | aux _ _ = NONE
     val (lhs, rhs) =
       case t of
@@ -1256,7 +1264,7 @@
     NONE
   else
     x |> def_props_for_const thy [(NONE, false)] false table |> List.last
-      |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
+      |> normalized_rhs_of |> Option.map (prefix_abs_vars s)
     handle List.Empty => NONE
 
 (* term -> fixpoint_kind *)
@@ -1366,13 +1374,12 @@
     ||> single |> op ::
   end
 (* theory -> string * typ list -> term list *)
-fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
+fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
   let val abs_T = Type abs_z in
     if is_univ_typedef thy abs_T then
       []
     else case typedef_info thy abs_s of
-      SOME {abs_type, rep_type, Abs_name, Rep_name, prop_of_Rep, set_name,
-            ...} =>
+      SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
       let
         val rep_T = instantiate_type thy abs_type abs_T rep_type
         val rep_t = Const (Rep_name, abs_T --> rep_T)
@@ -1495,7 +1502,7 @@
          [!simp_table, psimp_table]
 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 as {thy, def_table, ...}) =
+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)
 
@@ -1522,7 +1529,7 @@
   | is_constr_pattern _ (Var _) = true
   | is_constr_pattern thy t =
     case strip_comb t of
-      (Const (x as (s, _)), args) =>
+      (Const x, args) =>
       is_constr_like thy x andalso forall (is_constr_pattern thy) args
     | _ => false
 fun is_constr_pattern_lhs thy t =
@@ -1536,9 +1543,9 @@
 val unfold_max_depth = 255
 
 (* hol_context -> term -> term *)
-fun unfold_defs_in_term (hol_ctxt as {thy, stds, destroy_constrs, fast_descrs,
-                                      case_names, def_table, ground_thm_table,
-                                      ersatz_table, ...}) =
+fun unfold_defs_in_term (hol_ctxt as {thy, stds, fast_descrs, case_names,
+                                      def_table, ground_thm_table, ersatz_table,
+                                      ...}) =
   let
     (* int -> typ list -> term -> term *)
     fun do_term depth Ts t =
@@ -1566,8 +1573,7 @@
          handle SAME () => 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 (x as (@{const_name Sigma}, T))) $ t1
-        $ (t2 as Abs (_, _, t2')) =>
+      | (t0 as Const (@{const_name Sigma}, _)) $ t1 $ (t2 as Abs (_, _, t2')) =>
         betapplys (t0 |> loose_bvar1 (t2', 0) ? do_term depth Ts,
                    map (do_term depth Ts) [t1, t2])
       | Const (x as (@{const_name distinct},
@@ -1575,7 +1581,7 @@
         $ (t1 as _ $ _) =>
         (t1 |> HOLogic.dest_list |> distinctness_formula T'
          handle TERM _ => do_const depth Ts t x [t1])
-      | (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 =>
+      | Const (x as (@{const_name If}, _)) $ t1 $ t2 $ t3 =>
         if is_ground_term t1 andalso
            exists (Pattern.matches thy o rpair t1)
                   (Inttab.lookup_list ground_thm_table (hash_term t1)) then
@@ -1831,9 +1837,9 @@
              Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
            end
 
-(* typ list -> typ -> typ -> term -> term *)
-fun ap_curry [_] _ _ t = t
-  | ap_curry arg_Ts tuple_T body_T t =
+(* typ list -> typ -> term -> term *)
+fun ap_curry [_] _ t = t
+  | ap_curry arg_Ts tuple_T t =
     let val n = length arg_Ts in
       list_abs (map (pair "c") arg_Ts,
                 incr_boundvars n t
@@ -1843,7 +1849,7 @@
 (* int -> term -> int *)
 fun num_occs_of_bound_in_term j (t1 $ t2) =
     op + (pairself (num_occs_of_bound_in_term j) (t1, t2))
-  | num_occs_of_bound_in_term j (Abs (s, T, t')) =
+  | num_occs_of_bound_in_term j (Abs (_, _, t')) =
     num_occs_of_bound_in_term (j + 1) t'
   | num_occs_of_bound_in_term j (Bound j') = if j' = j then 1 else 0
   | num_occs_of_bound_in_term _ _ = 0
@@ -1917,8 +1923,7 @@
   in aux end
 
 (* hol_context -> styp -> term -> term *)
-fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (x as (s, T))
-                              def =
+fun starred_linear_pred_const (hol_ctxt as {simp_table, ...}) (s, T) def =
   let
     val j = maxidx_of_term def + 1
     val (outer, fp_app) = strip_abs def
@@ -1947,7 +1952,7 @@
                  $ (Const (@{const_name split}, curried_T --> uncurried_T)
                     $ list_comb (Const step_x, outer_bounds)))
               $ list_comb (Const base_x, outer_bounds)
-              |> ap_curry tuple_arg_Ts tuple_T bool_T)
+              |> ap_curry tuple_arg_Ts tuple_T)
     |> unfold_defs_in_term hol_ctxt
   end
 
@@ -2017,7 +2022,7 @@
 
 (* hol_context -> styp -> term list *)
 fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
-                                            psimp_table, ...}) (x as (s, _)) =
+                                            psimp_table, ...}) x =
   case def_props_for_const thy stds fast_descrs (!simp_table) x of
     [] => (case def_props_for_const thy stds fast_descrs psimp_table x of
              [] => [inductive_pred_axiom hol_ctxt x]
@@ -2044,7 +2049,7 @@
       | add_type _ table = table
     val table = fold (fold_types (fold_atyps add_type)) ts []
     (* typ -> typ *)
-    fun coalesce (TFree (s, S)) = TFree (AList.lookup (op =) table S |> the, S)
+    fun coalesce (TFree (_, S)) = TFree (AList.lookup (op =) table S |> the, S)
       | coalesce T = T
   in map (map_types (map_atyps coalesce)) ts end
 
@@ -2122,7 +2127,7 @@
 (* int list -> int list -> typ -> typ *)
 fun format_type default_format format T =
   let
-    val T = unarize_and_unbox_type T
+    val T = unarize_unbox_and_uniterize_type T
     val format = format |> filter (curry (op <) 0)
   in
     if forall (curry (op =) 1) format then
@@ -2172,14 +2177,14 @@
              ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n)
            val missing_vars = map nth_missing_var (0 upto length missing_js - 1)
            val vars = special_bounds ts @ missing_vars
-           val ts' = map2 (fn T => fn j =>
-                              case AList.lookup (op =) (js ~~ ts) j of
-                                SOME t => do_term t
-                              | NONE =>
-                                Var (nth missing_vars
-                                         (find_index (curry (op =) j)
-                                                     missing_js)))
-                          Ts (0 upto max_j)
+           val ts' =
+             map (fn j =>
+                     case AList.lookup (op =) (js ~~ ts) j of
+                       SOME t => do_term t
+                     | NONE =>
+                       Var (nth missing_vars
+                                (find_index (curry (op =) j) missing_js)))
+                 (0 upto max_j)
            val t = do_const x' |> fst
            val format =
              case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2)
@@ -2251,7 +2256,7 @@
          let val t = Const (original_name s, T) in
            (t, format_term_type thy def_table formats t)
          end)
-      |>> map_types unarize_and_unbox_type
+      |>> map_types unarize_unbox_and_uniterize_type
       |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name
   in do_const end
 
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -169,7 +169,7 @@
    | "false" => SOME false
    | "true" => SOME true
    | "" => SOME true
-   | s => raise Option)
+   | _ => raise Option)
   handle Option.Option =>
          let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
            error ("Parameter " ^ quote name ^ " must be assigned " ^
@@ -433,7 +433,6 @@
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
-    val thm = #goal (Proof.raw_goal state)
     val _ = List.app check_raw_param override_params
     val params as {blocking, debug, ...} =
       extract_params ctxt auto (default_raw_params thy) override_params
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -24,7 +24,7 @@
   val kk_tuple : bool -> int -> int list -> Kodkod.tuple
   val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
   val sequential_int_bounds : int -> Kodkod.int_bound list
-  val pow_of_two_int_bounds : int -> int -> int -> Kodkod.int_bound list
+  val pow_of_two_int_bounds : int -> int -> Kodkod.int_bound list
   val bounds_for_built_in_rels_in_formula :
     bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list
   val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
@@ -36,7 +36,7 @@
     hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
     -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
   val kodkod_formula_from_nut :
-    int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
+    int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
 end;
 
 structure Nitpick_Kodkod : NITPICK_KODKOD =
@@ -127,7 +127,7 @@
 (* int -> KK.int_bound list *)
 fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
 (* int -> int -> KK.int_bound list *)
-fun pow_of_two_int_bounds bits j0 univ_card =
+fun pow_of_two_int_bounds bits j0 =
   let
     (* int -> int -> int -> KK.int_bound list *)
     fun aux 0  _ _ = []
@@ -141,7 +141,7 @@
 fun built_in_rels_in_formula formula =
   let
     (* KK.rel_expr -> KK.n_ary_index list -> KK.n_ary_index list *)
-    fun rel_expr_func (r as KK.Rel (x as (n, j))) =
+    fun rel_expr_func (KK.Rel (x as (n, j))) =
         if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then
           I
         else
@@ -304,7 +304,7 @@
         (FreeRel (x, T as Type ("fun", [T1, T2]), R as Func (Atom (_, j0), R2),
                   nick)) =
     let
-      val constr as {delta, epsilon, exclusive, explicit_max, ...} =
+      val {delta, epsilon, exclusive, explicit_max, ...} =
         constr_spec dtypes (original_name nick, T1)
     in
       ([(x, bound_comment ctxt debug nick T R)],
@@ -511,7 +511,7 @@
         raise REP ("Nitpick_Kodkod.lone_rep_fallback", [old_R, new_R])
     end
 (* kodkod_constrs -> int * int -> rep -> KK.rel_expr -> KK.rel_expr *)
-and atom_from_rel_expr kk (x as (k, j0)) old_R r =
+and atom_from_rel_expr kk x old_R r =
   case old_R of
     Func (R1, R2) =>
     let
@@ -581,7 +581,7 @@
     end
   | func_from_no_opt_rel_expr kk Unit R2 old_R r =
     (case old_R of
-       Vect (k, R') => rel_expr_from_rel_expr kk R2 R' r
+       Vect (_, R') => rel_expr_from_rel_expr kk R2 R' r
      | Func (Unit, R2') => rel_expr_from_rel_expr kk R2 R2' r
      | Func (Atom (1, _), Formula Neut) =>
        (case unopt_rep R2 of
@@ -824,8 +824,8 @@
   nfa |> graph_for_nfa |> NfaGraph.strong_conn
       |> map (fn keys => filter (member (op =) keys o fst) nfa)
 
-(* kodkod_constrs -> dtype_spec list -> nfa_table -> typ -> KK.formula *)
-fun acyclicity_axiom_for_datatype kk dtypes nfa start_T =
+(* kodkod_constrs -> nfa_table -> typ -> KK.formula *)
+fun acyclicity_axiom_for_datatype kk nfa start_T =
   #kk_no kk (#kk_intersect kk
                  (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
 (* hol_context -> bool -> kodkod_constrs -> nut NameTable.table
@@ -834,20 +834,17 @@
   map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)
              dtypes
   |> strongly_connected_sub_nfas
-  |> maps (fn nfa =>
-              map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa)
+  |> maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa)
 
 (* hol_context -> bool -> int -> kodkod_constrs -> nut NameTable.table
    -> KK.rel_expr -> constr_spec -> int -> KK.formula *)
 fun sel_axiom_for_sel hol_ctxt binarize j0
-        (kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
-                kk_join, ...}) rel_table dom_r
-        ({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
+        (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
+        rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
         n =
   let
-    val x as (_, T) =
-      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
-    val (r, R, arity) = const_triple rel_table x
+    val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
+    val (r, R, _) = const_triple rel_table x
     val R2 = dest_Func R |> snd
     val z = (epsilon - delta, delta + j0)
   in
@@ -908,10 +905,6 @@
       map (const_triple rel_table
            o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
           (~1 upto num_sels - 1)
-    val j0 = case triples |> hd |> #2 of
-               Func (Atom (_, j0), _) => j0
-             | R => raise REP ("Nitpick_Kodkod.uniqueness_axiom_for_constr",
-                               [R])
     val set_r = triples |> hd |> #1
   in
     if num_sels = 0 then
@@ -962,8 +955,8 @@
   maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
        dtypes
 
-(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
-fun kodkod_formula_from_nut bits ofs
+(* int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
+fun kodkod_formula_from_nut ofs
         (kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
                 kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
                 kk_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
@@ -1098,7 +1091,7 @@
                 else
                   kk_subset (to_rep min_R u1) (to_rep min_R u2)
               end)
-         | Op2 (Eq, T, R, u1, u2) =>
+         | Op2 (Eq, _, _, u1, u2) =>
            (case min_rep (rep_of u1) (rep_of u2) of
               Unit => KK.True
             | Formula polar =>
@@ -1196,7 +1189,7 @@
       case u of
         Cst (False, _, Atom _) => false_atom
       | Cst (True, _, Atom _) => true_atom
-      | Cst (Iden, T, Func (Struct [R1, R2], Formula Neut)) =>
+      | Cst (Iden, _, Func (Struct [R1, R2], Formula Neut)) =>
         if R1 = R2 andalso arity_of_rep R1 = 1 then
           kk_intersect KK.Iden (kk_product (full_rel_for_rep R1) KK.Univ)
         else
@@ -1214,7 +1207,7 @@
                 (kk_rel_eq (rel_expr_from_rel_expr kk min_R R1 r1)
                            (rel_expr_from_rel_expr kk min_R R2 r2))
           end
-      | Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
+      | Cst (Iden, _, Func (Atom (1, j0), Formula Neut)) => KK.Atom j0
       | Cst (Iden, T as Type ("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) =>
@@ -1235,7 +1228,7 @@
         to_bit_word_unary_op T R (curry KK.Add (KK.Num 1))
       | 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 x, _)) => KK.Rel suc_rel
+      | 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) =>
@@ -1303,7 +1296,7 @@
       | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
         KK.Iden
       | Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
-             Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) =>
+             Func (Atom (_, nat_j0), Opt (Atom (int_k, int_j0)))) =>
         if nat_j0 = int_j0 then
           kk_intersect KK.Iden
               (kk_product (KK.AtomSeq (max_int_for_card int_k + 1, nat_j0))
@@ -1388,14 +1381,14 @@
         (case R of
            Func (R1, Formula Neut) => to_rep R1 u1
          | Func (Unit, Opt R) => to_guard [u1] R true_atom
-         | Func (R1, R2 as Opt _) =>
+         | Func (R1, Opt _) =>
            single_rel_rel_let kk
                (fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R)
                             (rel_expr_to_func kk R1 bool_atom_R
                                               (Func (R1, Formula Neut)) r))
                (to_opt R1 u1)
          | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u]))
-      | Op1 (Tha, T, R, u1) =>
+      | Op1 (Tha, _, R, u1) =>
         if is_opt_rep R then
           kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom
         else
@@ -1413,7 +1406,7 @@
       | Op2 (All, T, R as Opt _, u1, u2) =>
         to_r (Op1 (Not, T, R,
                    Op2 (Exist, T, R, u1, Op1 (Not, T, rep_of u2, u2))))
-      | Op2 (Exist, T, Opt _, u1, u2) =>
+      | Op2 (Exist, _, Opt _, u1, u2) =>
         let val rs1 = untuple to_decl u1 in
           if not (is_opt_rep (rep_of u2)) then
             kk_rel_if (kk_exist rs1 (to_f u2)) true_atom KK.None
@@ -1448,7 +1441,7 @@
                                 (int_expr_from_atom kk (type_of u1)) (r1, r2))))
                             KK.None)
                     (to_r u1) (to_r u2))
-      | Op2 (The, T, R, u1, u2) =>
+      | Op2 (The, _, R, u1, u2) =>
         if is_opt_rep R then
           let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in
             kk_rel_if (kk_one (kk_join r1 true_atom)) (kk_join r1 true_atom)
@@ -1461,7 +1454,7 @@
           let val r1 = to_rep (Func (R, Formula Neut)) u1 in
             kk_rel_if (kk_one r1) r1 (to_rep R u2)
           end
-      | Op2 (Eps, T, R, u1, u2) =>
+      | Op2 (Eps, _, R, u1, u2) =>
         if is_opt_rep (rep_of u1) then
           let
             val r1 = to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1
@@ -1483,7 +1476,7 @@
                      (kk_rel_if (kk_or (kk_no r1) (kk_subset r2 r1))
                                 r2 (empty_rel_for_rep R))
           end
-      | Op2 (Triad, T, Opt (Atom (2, j0)), u1, u2) =>
+      | Op2 (Triad, _, Opt (Atom (2, j0)), u1, u2) =>
         let
           val f1 = to_f u1
           val f2 = to_f u2
@@ -1608,11 +1601,11 @@
           false_atom
         else
           to_apply R u1 u2
-      | Op2 (Lambda, T, R as Opt (Atom (1, j0)), u1, u2) =>
+      | Op2 (Lambda, _, R as Opt (Atom (1, j0)), u1, u2) =>
         to_guard [u1, u2] R (KK.Atom j0)
-      | Op2 (Lambda, T, Func (_, Formula Neut), u1, u2) =>
+      | Op2 (Lambda, _, Func (_, Formula Neut), u1, u2) =>
         kk_comprehension (untuple to_decl u1) (to_f u2)
-      | Op2 (Lambda, T, Func (_, R2), u1, u2) =>
+      | Op2 (Lambda, _, Func (_, R2), u1, u2) =>
         let
           val dom_decls = untuple to_decl u1
           val ran_schema = atom_schema_of_rep R2
@@ -1650,7 +1643,7 @@
                                (KK.Atom j0) KK.None)
          | _ => raise NUT ("Nitpick_Kodkod.to_r (Tuple)", [u]))
       | Construct ([u'], _, _, []) => to_r u'
-      | Construct (discr_u :: sel_us, T, R, arg_us) =>
+      | Construct (discr_u :: sel_us, _, _, arg_us) =>
         let
           val set_rs =
             map2 (fn sel_u => fn arg_u =>
@@ -1676,7 +1669,7 @@
         KK.DeclOne (x, KK.AtomSeq (the_single (atom_schema_of_rep R)))
       | to_decl u = raise NUT ("Nitpick_Kodkod.to_decl", [u])
     (* nut -> KK.expr_assign *)
-    and to_expr_assign (FormulaReg (j, _, R)) u =
+    and to_expr_assign (FormulaReg (j, _, _)) u =
         KK.AssignFormulaReg (j, to_f u)
       | to_expr_assign (RelReg (j, _, R)) u =
         KK.AssignRelReg ((arity_of_rep R, j), to_r u)
@@ -1775,7 +1768,7 @@
                case arity_of_rep nth_R of
                  0 => to_guard [u] res_R
                                (to_rep res_R (Cst (Unity, res_T, Unit)))
-               | arity => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0
+               | _ => to_project res_R nth_R (to_rep (Opt (Struct Rs)) u) j0
              end
     (* (KK.formula -> KK.formula -> KK.formula)
        -> (KK.rel_expr -> KK.rel_expr -> KK.formula) -> nut -> nut
@@ -1788,11 +1781,11 @@
       in
         case min_R of
           Vect (k, Atom _) => kk_vect_set_bool_op connective k r1 r2
-        | Func (R1, Formula Neut) => set_oper r1 r2
+        | Func (_, Formula Neut) => set_oper r1 r2
         | Func (Unit, Atom (2, j0)) =>
           connective (formula_from_atom j0 r1) (formula_from_atom j0 r2)
-        | Func (R1, Atom _) => set_oper (kk_join r1 true_atom)
-                                        (kk_join r2 true_atom)
+        | Func (_, Atom _) => set_oper (kk_join r1 true_atom)
+                                       (kk_join r2 true_atom)
         | _ => raise REP ("Nitpick_Kodkod.to_set_bool_op", [min_R])
       end
     (* (KK.formula -> KK.formula -> KK.formula)
@@ -1815,7 +1808,7 @@
              | Vect (k, Atom _) => kk_vect_set_op connective k r1 r2
              | Func (_, Formula Neut) => set_oper r1 r2
              | Func (Unit, _) => connective3 r1 r2
-             | Func (R1, _) =>
+             | Func _ =>
                double_rel_rel_let kk
                    (fn r1 => fn r2 =>
                        kk_union
@@ -1877,7 +1870,7 @@
       | Atom (1, j0) =>
         to_guard [arg_u] res_R
                  (rel_expr_from_rel_expr kk res_R (Atom (1, j0)) (to_r func_u))
-      | Atom (k, j0) =>
+      | Atom (k, _) =>
         let
           val dom_card = card_of_rep (rep_of arg_u)
           val ran_R = Atom (exact_root dom_card k,
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -74,12 +74,12 @@
   |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
      ? prefix "\<^isub>,"
 (* atom_pool Unsynchronized.ref -> string -> typ -> int -> int -> string *)
-fun nth_atom_name pool prefix (T as Type (s, _)) j k =
+fun nth_atom_name pool prefix (Type (s, _)) j k =
     let val s' = shortest_name s in
       prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
       nth_atom_suffix pool s j k
     end
-  | nth_atom_name pool prefix (T as TFree (s, _)) j k =
+  | nth_atom_name pool prefix (TFree (s, _)) j k =
     prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
   | nth_atom_name _ _ T _ _ =
     raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
@@ -113,20 +113,23 @@
 fun unarize_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
     unarize_and_unbox_term t1
   | unarize_and_unbox_term (Const (@{const_name PairBox},
-                                   Type ("fun", [T1, Type ("fun", [T2, T3])]))
+                                   Type ("fun", [T1, Type ("fun", [T2, _])]))
                             $ t1 $ t2) =
-    let val Ts = map unarize_and_unbox_type [T1, T2] in
+    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
     end
-  | unarize_and_unbox_term (Const (s, T)) = Const (s, unarize_and_unbox_type T)
+  | 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_and_unbox_type T)
-  | unarize_and_unbox_term (Var (x, T)) = Var (x, unarize_and_unbox_type T)
+  | 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_and_unbox_type T, unarize_and_unbox_term t')
+    Abs (s, unarize_unbox_and_uniterize_type T, unarize_and_unbox_term t')
 
 (* typ -> typ -> (typ * typ) * (typ * typ) *)
 fun factor_out_types (T1 as Type ("*", [T11, T12]))
@@ -260,12 +263,12 @@
   | mk_tuple _ (t :: _) = t
   | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
 
-(* bool -> atom_pool -> string * string * string * string -> scope -> nut list
-   -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
-   -> typ -> rep -> int list list -> term *)
-fun reconstruct_term unfold pool (maybe_name, base_name, step_name, abs_name)
-        ({hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns, bits,
-          datatypes, ofs, ...} : scope) sel_names rel_table bounds =
+(* bool -> atom_pool -> (string * string) * (string * string) -> scope
+   -> nut list -> nut list -> nut list -> nut NameTable.table
+   -> KK.raw_bound list -> typ -> typ -> rep -> int list list -> term *)
+fun reconstruct_term unfold pool ((maybe_name, abs_name), _)
+        ({hol_ctxt as {thy, stds, ...}, binarize, card_assigns, bits, datatypes,
+          ofs, ...} : scope) sel_names rel_table bounds =
   let
     val for_auto = (maybe_name = "")
     (* int list list -> int *)
@@ -357,11 +360,11 @@
       ts1 ~~ ts2 |> sort (nice_term_ord o pairself fst)
                  |> make_plain_fun maybe_opt T1 T2
                  |> unarize_and_unbox_term
-                 |> typecast_fun (unarize_and_unbox_type T')
-                                 (unarize_and_unbox_type T1)
-                                 (unarize_and_unbox_type T2)
+                 |> typecast_fun (unarize_unbox_and_uniterize_type T')
+                                 (unarize_unbox_and_uniterize_type T1)
+                                 (unarize_unbox_and_uniterize_type T2)
     (* (typ * int) list -> typ -> typ -> int -> term *)
-    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j k =
+    fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j _ =
         let
           val k1 = card_of_type card_assigns T1
           val k2 = card_of_type card_assigns T2
@@ -525,7 +528,7 @@
                      map3 (fn T => term_for_rep seen T T) [T1, T2] [R1, R2]
                           [[js1], [js2]])
         end
-      | term_for_rep seen (Type ("fun", [T1, T2])) T' (R as Vect (k, R')) [js] =
+      | term_for_rep seen (Type ("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 =
@@ -548,7 +551,7 @@
         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 seen 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))
@@ -559,11 +562,11 @@
 fun term_for_name pool scope sel_names rel_table bounds name =
   let val T = type_of name in
     tuple_list_for_name rel_table bounds name
-    |> reconstruct_term false pool ("", "", "", "") scope sel_names rel_table
-                        bounds T T (rep_of name)
+    |> reconstruct_term false pool (("", ""), ("", "")) scope sel_names
+                        rel_table bounds T T (rep_of name)
   end
 
-(* Proof.context -> (string * string * string * string) * Proof.context *)
+(* Proof.context -> ((string * string) * (string * string)) * Proof.context *)
 fun add_wacky_syntax ctxt =
   let
     (* term -> string *)
@@ -572,17 +575,17 @@
     val (maybe_t, thy) =
       Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
                           Mixfix (maybe_mixfix, [1000], 1000)) thy
+    val (abs_t, thy) =
+      Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
+                          Mixfix (abs_mixfix, [40], 40)) thy
     val (base_t, thy) =
       Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
                           Mixfix (base_mixfix, [1000], 1000)) thy
     val (step_t, thy) =
       Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
                           Mixfix (step_mixfix, [1000], 1000)) thy
-    val (abs_t, thy) =
-      Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
-                          Mixfix (abs_mixfix, [40], 40)) thy
   in
-    ((name_of maybe_t, name_of base_t, name_of step_t, name_of abs_t),
+    (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
      ProofContext.transfer_syntax thy ctxt)
   end
 
@@ -613,18 +616,18 @@
   -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list
   -> Pretty.T * bool *)
 fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
-        ({hol_ctxt as {thy, ctxt, max_bisim_depth, boxes, stds, wfs,
-                       user_axioms, debug, binary_ints, destroy_constrs,
-                       specialize, skolemize, star_linear_preds, uncurry,
-                       fast_descrs, tac_timeout, evals, case_names, def_table,
-                       nondef_table, user_nondefs, simp_table, psimp_table,
-                       intro_table, ground_thm_table, ersatz_table, skolems,
-                       special_funs, unrolled_preds, wf_cache, constr_cache},
+        ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
+                      debug, binary_ints, destroy_constrs, specialize,
+                      skolemize, star_linear_preds, uncurry, fast_descrs,
+                      tac_timeout, evals, case_names, def_table, nondef_table,
+                      user_nondefs, simp_table, psimp_table, intro_table,
+                      ground_thm_table, ersatz_table, skolems, special_funs,
+                      unrolled_preds, wf_cache, constr_cache},
          binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
         formats all_frees free_names sel_names nonsel_names rel_table bounds =
   let
     val pool = Unsynchronized.ref []
-    val (wacky_names as (_, base_name, step_name, _), ctxt) =
+    val (wacky_names as (_, base_step_names), ctxt) =
       add_wacky_syntax ctxt
     val hol_ctxt =
       {thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
@@ -679,13 +682,12 @@
         val (oper, (t1, T'), T) =
           case name of
             FreeName (s, T, _) =>
-            let val t = Free (s, unarize_and_unbox_type T) in
+            let val t = Free (s, unarize_unbox_and_uniterize_type T) in
               ("=", (t, format_term_type thy def_table formats t), T)
             end
           | ConstName (s, T, _) =>
             (assign_operator_for_const (s, T),
-             user_friendly_const hol_ctxt (base_name, step_name) formats (s, T),
-             T)
+             user_friendly_const hol_ctxt base_step_names formats (s, T), T)
           | _ => raise NUT ("Nitpick_Model.reconstruct_hol_model.\
                             \pretty_for_assign", [name])
         val t2 = if rep_of name = Any then
@@ -701,7 +703,8 @@
     (* dtype_spec -> Pretty.T *)
     fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
       Pretty.block (Pretty.breaks
-          [Syntax.pretty_typ ctxt (unarize_and_unbox_type typ), Pretty.str "=",
+          [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 complete then [] else [Pretty.str unrep]))])
@@ -746,7 +749,8 @@
     val free_names =
       map (fn x as (s, T) =>
               case filter (curry (op =) x
-                       o pairf nickname_of (unarize_and_unbox_type o type_of))
+                       o pairf nickname_of
+                               (unarize_unbox_and_uniterize_type o type_of))
                        free_names of
                 [name] => name
               | [] => FreeName (s, T, Any)
@@ -767,7 +771,7 @@
 
 (* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
    -> KK.raw_bound list -> term -> bool option *)
-fun prove_hol_model (scope as {hol_ctxt as {thy, ctxt, debug, ...},
+fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
                                card_assigns, ...})
                     auto_timeout free_names sel_names rel_table bounds prop =
   let
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -45,7 +45,7 @@
 exception CTYPE of string * ctype list
 
 (* string -> unit *)
-fun print_g (s : string) = ()
+fun print_g (_ : string) = ()
 
 (* var -> string *)
 val string_for_var = signed_string_of_int
@@ -265,7 +265,7 @@
   end
 
 (* cdata -> styp -> ctype *)
-fun ctype_for_constr (cdata as {hol_ctxt as {thy, ...}, alpha_T, constr_cache,
+fun ctype_for_constr (cdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
                                 ...}) (x as (_, T)) =
   if could_exist_alpha_sub_ctype thy alpha_T T then
     case AList.lookup (op =) (!constr_cache) x of
@@ -339,7 +339,7 @@
      | (S Minus, S Plus) => NONE
      | (V _, V _) => SOME (lits, insert (op =) (a1, a2, Leq, []) comps)
      | _ => do_sign_atom_comp Eq [] a1 a2 accum)
-  | do_sign_atom_comp cmp xs a1 a2 (accum as (lits, comps)) =
+  | do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
     SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
 
 (* comp -> var list -> ctype -> ctype -> (literal list * comp list) option
@@ -367,7 +367,7 @@
     (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]
      handle Library.UnequalLengths =>
             raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]))
-  | do_ctype_comp cmp xs (CType _) (CType _) accum =
+  | do_ctype_comp _ _ (CType _) (CType _) accum =
     accum (* no need to compare them thanks to the cache *)
   | do_ctype_comp _ _ C1 C2 _ =
     raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])
@@ -435,13 +435,6 @@
 val add_ctype_is_right_unique = add_notin_ctype_fv Minus
 val add_ctype_is_right_total = add_notin_ctype_fv Plus
 
-(* constraint_set -> constraint_set -> constraint_set *)
-fun unite (CSet (lits1, comps1, sexps1)) (CSet (lits2, comps2, sexps2)) =
-    (case SOME lits1 |> fold do_literal lits2 of
-       NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
-     | SOME lits => CSet (lits, comps1 @ comps2, sexps1 @ sexps2))
-  | unite _ _ = UnsolvableCSet
-
 (* sign -> bool *)
 fun bool_from_sign Plus = false
   | bool_from_sign Minus = true
@@ -480,10 +473,6 @@
              SOME b => (x, sign_from_bool b) :: accum
            | NONE => accum) (max_var downto 1) lits
 
-(* literal list -> sign_atom -> sign option *)
-fun lookup_sign_atom _ (S sn) = SOME sn
-  | lookup_sign_atom lit (V x) = AList.lookup (op =) lit x
-
 (* comp -> string *)
 fun string_for_comp (a1, a2, cmp, xs) =
   string_for_sign_atom a1 ^ " " ^ string_for_comp_op cmp ^
@@ -522,9 +511,6 @@
       | _ => NONE
     end
 
-(* var -> constraint_set -> bool *)
-val is_solvable = is_some oo solve
-
 type ctype_schema = ctype * constraint_set
 type ctype_context =
   {bounds: ctype list,
@@ -545,8 +531,8 @@
   handle List.Empty => initial_gamma
 
 (* cdata -> term -> accumulator -> ctype * accumulator *)
-fun consider_term (cdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
-                                          def_table, ...},
+fun consider_term (cdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
+                                         def_table, ...},
                              alpha_T, max_fresh, ...}) =
   let
     (* typ -> ctype *)
@@ -765,7 +751,7 @@
          | Var _ => (print_g "*** Var"; unsolvable)
          | Bound j => (nth bounds j, accum)
          | Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum)
-         | Abs (s, T, t') =>
+         | Abs (_, T, t') =>
            ((case t' of
                t1' $ Bound 0 =>
                if not (loose_bvar1 (t1', 0)) then
@@ -806,7 +792,7 @@
   in do_term end
 
 (* cdata -> sign -> term -> accumulator -> accumulator *)
-fun consider_general_formula (cdata as {hol_ctxt as {ctxt, ...}, ...}) =
+fun consider_general_formula (cdata as {hol_ctxt = {ctxt, ...}, ...}) =
   let
     (* typ -> ctype *)
     val ctype_for = fresh_ctype_for_type cdata
@@ -814,7 +800,7 @@
     val do_term = consider_term cdata
     (* sign -> term -> accumulator -> accumulator *)
     fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
-      | do_formula sn t (accum as (gamma as {bounds, frees, consts}, cset)) =
+      | do_formula sn t (accum as (gamma, cset)) =
         let
           (* term -> accumulator -> accumulator *)
           val do_co_formula = do_formula sn
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -7,7 +7,6 @@
 
 signature NITPICK_NUT =
 sig
-  type special_fun = Nitpick_HOL.special_fun
   type hol_context = Nitpick_HOL.hol_context
   type scope = Nitpick_Scope.scope
   type name_pool = Nitpick_Peephole.name_pool
@@ -467,7 +466,7 @@
   | factorize z = [z]
 
 (* hol_context -> op2 -> term -> nut *)
-fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, special_funs, ...}) eq =
+fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, ...}) eq =
   let
     (* string list -> typ list -> term -> nut *)
     fun aux eq ss Ts t =
@@ -518,11 +517,21 @@
             val t1 = list_comb (t0, ts')
             val T1 = fastype_of1 (Ts, t1)
           in Op2 (Apply, range_type T1, Any, sub t1, sub t2) end
+        (* styp -> term list -> term *)
+        fun construct (x as (_, T)) ts =
+          case num_binder_types T - length ts of
+            0 => Construct (map ((fn (s', T') => ConstName (s', T', Any))
+                                  o nth_sel_for_constr x)
+                                (~1 upto num_sels_for_constr_type T - 1),
+                            body_type T, Any,
+                            ts |> map (`(curry fastype_of1 Ts))
+                               |> maps factorize |> map (sub o snd))
+          | k => sub (eta_expand Ts t k)
       in
         case strip_comb t of
           (Const (@{const_name all}, _), [Abs (s, T, t1)]) =>
           do_quantifier All s T t1
-        | (t0 as Const (@{const_name all}, T), [t1]) =>
+        | (t0 as Const (@{const_name all}, _), [t1]) =>
           sub' (t0 $ eta_expand Ts t1 1)
         | (Const (@{const_name "=="}, T), [t1, t2]) => sub_equals T t1 t2
         | (Const (@{const_name "==>"}, _), [t1, t2]) =>
@@ -538,11 +547,11 @@
         | (Const (@{const_name True}, T), []) => Cst (True, T, Any)
         | (Const (@{const_name All}, _), [Abs (s, T, t1)]) =>
           do_quantifier All s T t1
-        | (t0 as Const (@{const_name All}, T), [t1]) =>
+        | (t0 as Const (@{const_name All}, _), [t1]) =>
           sub' (t0 $ eta_expand Ts t1 1)
         | (Const (@{const_name Ex}, _), [Abs (s, T, t1)]) =>
           do_quantifier Exist s T t1
-        | (t0 as Const (@{const_name Ex}, T), [t1]) =>
+        | (t0 as Const (@{const_name Ex}, _), [t1]) =>
           sub' (t0 $ eta_expand Ts t1 1)
         | (t0 as Const (@{const_name The}, T), [t1]) =>
           if fast_descrs then
@@ -568,7 +577,7 @@
         | (Const (@{const_name Let}, T), [t1, Abs (s, T', t2)]) =>
           Op3 (Let, nth_range_type 2 T, Any, BoundName (length Ts, T', Any, s),
                sub t1, sub_abs s T' t2)
-        | (t0 as Const (@{const_name Let}, T), [t1, t2]) =>
+        | (t0 as Const (@{const_name Let}, _), [t1, t2]) =>
           sub (t0 $ t1 $ eta_expand Ts t2 1)
         | (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any)
         | (Const (@{const_name Pair}, T), [t1, t2]) =>
@@ -595,7 +604,10 @@
           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 (@{const_name Suc}, T), []) => Cst (Suc, T, Any)
+        | (Const (x as (s as @{const_name Suc}, T)), []) =>
+          if is_built_in_const thy stds false x then Cst (Suc, T, Any)
+          else if is_constr thy stds x then construct x []
+          else ConstName (s, T, Any)
         | (Const (@{const_name finite}, T), [t1]) =>
           (if is_finite_type hol_ctxt (domain_type T) then
              Cst (True, bool_T, Any)
@@ -604,14 +616,9 @@
            | _ => Op1 (Finite, bool_T, Any, sub t1))
         | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
         | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
-          if is_built_in_const thy stds false x then
-            Cst (Num 0, T, Any)
-          else if is_constr thy stds x then
-            let val (s', T') = discr_for_constr x in
-              Construct ([ConstName (s', T', Any)], T, Any, [])
-            end
-          else
-            ConstName (s, T, Any)
+          if is_built_in_const thy stds false x then Cst (Num 0, T, Any)
+          else if is_constr thy stds x then construct x []
+          else ConstName (s, T, Any)
         | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
           if is_built_in_const thy stds false x then Cst (Num 1, T, Any)
           else ConstName (s, T, Any)
@@ -631,7 +638,7 @@
         | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
           if is_built_in_const thy stds false x then Cst (Divide, T, Any)
           else ConstName (s, T, Any)
-        | (t0 as Const (x as (s as @{const_name ord_class.less}, T)),
+        | (t0 as Const (x as (@{const_name ord_class.less}, _)),
            ts as [t1, t2]) =>
           if is_built_in_const thy stds false x then
             Op2 (Less, bool_T, Any, sub t1, sub t2)
@@ -642,7 +649,7 @@
            [t1, t2]) =>
           Op2 (Subset, bool_T, Any, sub t1, sub t2)
         (* FIXME: find out if this case is necessary *)
-        | (t0 as Const (x as (s as @{const_name ord_class.less_eq}, T)),
+        | (t0 as Const (x as (@{const_name ord_class.less_eq}, _)),
            ts as [t1, t2]) =>
           if is_built_in_const thy stds false x then
             Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
@@ -660,7 +667,7 @@
           else
             ConstName (s, T, Any)
         | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
-        | (Const (@{const_name is_unknown}, T), [t1]) =>
+        | (Const (@{const_name is_unknown}, _), [t1]) =>
           Op1 (IsUnknown, bool_T, Any, sub t1)
         | (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
           Op1 (Tha, T2, Any, sub t1)
@@ -681,14 +688,7 @@
           Op2 (Union, T1, Any, sub t1, sub t2)
         | (t0 as Const (x as (s, T)), ts) =>
           if is_constr thy stds x then
-            case num_binder_types T - length ts of
-              0 => Construct (map ((fn (s, T) => ConstName (s, T, Any))
-                                    o nth_sel_for_constr x)
-                                  (~1 upto num_sels_for_constr_type T - 1),
-                              body_type T, Any,
-                              ts |> map (`(curry fastype_of1 Ts))
-                                 |> maps factorize |> map (sub o snd))
-            | k => sub (eta_expand Ts t k)
+            construct x ts
           else if String.isPrefix numeral_prefix s then
             Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
           else
@@ -726,8 +726,8 @@
   in (v :: vs, NameTable.update (v, R) table) end
 (* scope -> bool -> nut -> nut list * rep NameTable.table
    -> nut list * rep NameTable.table *)
-fun choose_rep_for_const (scope as {hol_ctxt as {thy, ctxt, ...}, datatypes,
-                                    ofs, ...}) all_exact v (vs, table) =
+fun choose_rep_for_const (scope as {hol_ctxt = {thy, ...}, ...}) all_exact v
+                         (vs, table) =
   let
     val x as (s, T) = (nickname_of v, type_of v)
     val R = (if is_abs_fun thy x then
@@ -904,8 +904,7 @@
   | untuple f u = if rep_of u = Unit then [] else [f u]
 
 (* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
-fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
-                                  bits, datatypes, ofs, ...})
+fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
                        unsound table def =
   let
     val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
@@ -991,7 +990,7 @@
             Cst (cst, T, best_set_rep_for_type scope T)
         | Op1 (Not, T, _, u1) =>
           (case gsub def (flip_polarity polar) u1 of
-             Op2 (Triad, T, R, u11, u12) =>
+             Op2 (Triad, T, _, u11, u12) =>
              triad (s_op1 Not T (Formula Pos) u12)
                    (s_op1 Not T (Formula Neg) u11)
            | u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1')
@@ -1138,7 +1137,7 @@
                  else
                    unopt_rep R
              in s_op2 Lambda T R u1' u2' end
-           | R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
+           | _ => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
         | Op2 (oper, T, _, u1, u2) =>
           if oper = All orelse oper = Exist then
             let
@@ -1307,7 +1306,7 @@
     end
   | shape_tuple (T as Type ("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 R [u] =
+  | shape_tuple T _ [u] =
     if type_of u = T then u else raise NUT ("Nitpick_Nut.shape_tuple", [u])
   | shape_tuple T Unit [] = Cst (Unity, T, Unit)
   | shape_tuple _ _ us = raise NUT ("Nitpick_Nut.shape_tuple", us)
@@ -1390,7 +1389,6 @@
       let
         val bs = untuple I u1
         val (_, pool, table') = fold rename_plain_var bs ([], pool, table)
-        val u11 = rename_vars_in_nut pool table' u1
       in
         Op3 (Let, T, R, rename_vars_in_nut pool table' u1,
              rename_vars_in_nut pool table u2,
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_peephole.ML
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -261,14 +261,10 @@
 (* bool -> int -> int -> int -> kodkod_constrs *)
 fun kodkod_constrs optim nat_card int_card main_j0 =
   let
-    val false_atom = Atom main_j0
-    val true_atom = Atom (main_j0 + 1)
-
     (* bool -> int *)
     val from_bool = atom_for_bool main_j0
     (* int -> rel_expr *)
     fun from_nat n = Atom (n + main_j0)
-    val from_int = Atom o atom_for_int (int_card, main_j0)
     (* int -> int *)
     fun to_nat j = j - main_j0
     val to_int = int_for_atom (int_card, main_j0)
@@ -415,7 +411,7 @@
     fun s_subset (Atom j1) (Atom j2) = formula_for_bool (j1 = j2)
       | s_subset (Atom j) (AtomSeq (k, j0)) =
         formula_for_bool (j >= j0 andalso j < j0 + k)
-      | s_subset (r1 as Union (r11, r12)) r2 =
+      | s_subset (Union (r11, r12)) r2 =
         s_and (s_subset r11 r2) (s_subset r12 r2)
       | s_subset r1 (r2 as Union (r21, r22)) =
         if is_one_rel_expr r1 then
@@ -516,7 +512,7 @@
       | s_join (r1 as RelIf (f, r11, r12)) r2 =
         if inline_rel_expr r2 then s_rel_if f (s_join r11 r2) (s_join r12 r2)
         else Join (r1, r2)
-      | s_join (r1 as Atom j1) (r2 as Rel (x as (2, j2))) =
+      | s_join (r1 as Atom j1) (r2 as Rel (x as (2, _))) =
         if x = suc_rel then
           let val n = to_nat j1 + 1 in
             if n < nat_card then from_nat n else None
@@ -528,7 +524,7 @@
           s_project (s_join r21 r1) is
         else
           Join (r1, r2)
-      | s_join r1 (Join (r21, r22 as Rel (x as (3, j22)))) =
+      | s_join r1 (Join (r21, r22 as Rel (x as (3, _)))) =
         ((if x = nat_add_rel then
             case (r21, r1) of
               (Atom j1, Atom j2) =>
@@ -613,7 +609,6 @@
       in aux (arity_of_rel_expr r) r end
 
     (* rel_expr -> rel_expr -> rel_expr *)
-    fun s_nat_subtract r1 r2 = fold s_join [r1, r2] (Rel nat_subtract_rel)
     fun s_nat_less (Atom j1) (Atom j2) = from_bool (j1 < j2)
       | s_nat_less r1 r2 = fold s_join [r1, r2] (Rel nat_less_rel)
     fun s_int_less (Atom j1) (Atom j2) = from_bool (to_int j1 < to_int j2)
@@ -624,7 +619,6 @@
     (* rel_expr -> rel_expr *)
     fun d_not3 r = Join (r, Rel not3_rel)
     (* rel_expr -> rel_expr -> rel_expr *)
-    fun d_nat_subtract r1 r2 = List.foldl Join (Rel nat_subtract_rel) [r1, r2]
     fun d_nat_less r1 r2 = List.foldl Join (Rel nat_less_rel) [r1, r2]
     fun d_int_less r1 r2 = List.foldl Join (Rel int_less_rel) [r1, r2]
   in
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -87,10 +87,9 @@
            SOME n =>
            if n >= 2 then
              let
-               val (arg_Ts, rest_T) = strip_n_binders n T
+               val arg_Ts = strip_n_binders n T |> fst
                val j =
-                 if hd arg_Ts = @{typ bisim_iterator} orelse
-                    is_fp_iterator_type (hd arg_Ts) then
+                 if is_iterator_type (hd arg_Ts) then
                    1
                  else case find_index (not_equal bool_T) arg_Ts of
                    ~1 => n
@@ -363,8 +362,8 @@
 fun fresh_value_var Ts k n j t =
   Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
 
-(* typ list -> int -> term -> bool *)
-fun has_heavy_bounds_or_vars Ts level t =
+(* typ list -> term -> bool *)
+fun has_heavy_bounds_or_vars Ts t =
   let
     (* typ list -> bool *)
     fun aux [] = false
@@ -381,7 +380,7 @@
       Const x =>
       if not relax andalso is_constr thy stds x andalso
          not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
-         has_heavy_bounds_or_vars Ts level t_comb andalso
+         has_heavy_bounds_or_vars Ts t_comb andalso
          not (loose_bvar (t_comb, level)) then
         let
           val (j, seen) = case find_index (curry (op =) t_comb) seen of
@@ -629,7 +628,7 @@
            $ Abs (s, T, kill ss Ts ts))
       | kill _ _ _ = raise UnequalLengths
     (* string list -> typ list -> term -> term *)
-    fun gather ss Ts ((t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1)) =
+    fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
         gather (ss @ [s1]) (Ts @ [T1]) t1
       | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
       | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
@@ -704,7 +703,7 @@
         | @{const "op -->"} $ t1 $ t2 =>
           @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
           $ aux ss Ts js depth polar t2
-        | (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
+        | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
           t0 $ t1 $ aux ss Ts js depth polar t2
         | Const (x as (s, T)) =>
           if is_inductive_pred hol_ctxt x andalso
@@ -843,7 +842,7 @@
 val bound_var_prefix = "b"
 
 (* hol_context -> int -> term -> term *)
-fun specialize_consts_in_term (hol_ctxt as {thy, specialize, simp_table,
+fun specialize_consts_in_term (hol_ctxt as {specialize, simp_table,
                                             special_funs, ...}) depth t =
   if not specialize orelse depth > special_max_depth then
     t
@@ -919,8 +918,8 @@
 
 val cong_var_prefix = "c"
 
-(* styp -> special_triple -> special_triple -> term *)
-fun special_congruence_axiom (s, T) (js1, ts1, x1) (js2, ts2, x2) =
+(* typ -> special_triple -> special_triple -> term *)
+fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) =
   let
     val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
     val Ts = binder_types T
@@ -959,28 +958,28 @@
     fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
       x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
                                       (j2 ~~ t2, j1 ~~ t1)
-    (* styp -> special_triple list -> special_triple list -> special_triple list
+    (* typ -> special_triple list -> special_triple list -> special_triple list
        -> term list -> term list *)
     fun do_pass_1 _ [] [_] [_] = I
-      | do_pass_1 x skipped _ [] = do_pass_2 x skipped
-      | do_pass_1 x skipped all (z :: zs) =
+      | do_pass_1 T skipped _ [] = do_pass_2 T skipped
+      | do_pass_1 T skipped all (z :: zs) =
         case filter (is_more_specific z) all
              |> sort (int_ord o pairself generality) of
-          [] => do_pass_1 x (z :: skipped) all zs
-        | (z' :: _) => cons (special_congruence_axiom x z z')
-                       #> do_pass_1 x skipped all zs
-    (* styp -> special_triple list -> term list -> term list *)
+          [] => do_pass_1 T (z :: skipped) all zs
+        | (z' :: _) => cons (special_congruence_axiom T z z')
+                       #> do_pass_1 T skipped all zs
+    (* typ -> special_triple list -> term list -> term list *)
     and do_pass_2 _ [] = I
-      | do_pass_2 x (z :: zs) =
-        fold (cons o special_congruence_axiom x z) zs #> do_pass_2 x zs
-  in fold (fn (x, zs) => do_pass_1 x [] zs zs) groups [] end
+      | do_pass_2 T (z :: zs) =
+        fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs
+  in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end
 
 (** Axiom selection **)
 
 (* Similar to "Refute.specialize_type" but returns all matches rather than only
    the first (preorder) match. *)
 (* theory -> styp -> term -> term list *)
-fun multi_specialize_type thy slack (x as (s, T)) t =
+fun multi_specialize_type thy slack (s, T) t =
   let
     (* term -> (typ * term) list -> (typ * term) list *)
     fun aux (Const (s', T')) ys =
@@ -1062,7 +1061,7 @@
             is_built_in_const thy stds fast_descrs x then
            accum
          else
-           let val accum as (xs, _) = (x :: xs, axs) in
+           let val accum = (x :: xs, axs) in
              if depth > axioms_max_depth then
                raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
                                 \add_axioms_for_term",
@@ -1130,7 +1129,7 @@
       | @{typ unit} => I
       | TFree (_, S) => add_axioms_for_sort depth T S
       | TVar (_, S) => add_axioms_for_sort depth T S
-      | Type (z as (s, Ts)) =>
+      | Type (z as (_, Ts)) =>
         fold (add_axioms_for_type depth) Ts
         #> (if is_pure_typedef thy T then
               fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
@@ -1192,7 +1191,7 @@
         ((if is_constr_like thy x then
             if length args = num_binder_types T then
               case hd args of
-                Const (x' as (_, T')) $ t' =>
+                Const (_, T') $ t' =>
                 if domain_type T' = body_type T andalso
                    forall (uncurry (is_nth_sel_on t'))
                           (index_seq 0 (length args) ~~ args) then
@@ -1276,13 +1275,13 @@
    paper). *)
 val quantifier_cluster_threshold = 7
 
-(* theory -> term -> term *)
-fun push_quantifiers_inward thy =
+(* term -> term *)
+val push_quantifiers_inward =
   let
     (* string -> string list -> typ list -> term -> term *)
     fun aux quant_s ss Ts t =
       (case t of
-         (t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
+         Const (s0, _) $ Abs (s1, T1, t1 as _ $ _) =>
          if s0 = quant_s then
            aux s0 (s1 :: ss) (T1 :: Ts) t1
          else if quant_s = "" andalso
@@ -1406,8 +1405,8 @@
     val table =
       Termtab.empty |> uncurry
         ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
-    (* bool -> bool -> term -> term *)
-    fun do_rest def core =
+    (* bool -> term -> term *)
+    fun do_rest def =
       binarize ? binarize_nat_and_int_in_term
       #> uncurry ? uncurry_term table
       #> box ? box_fun_and_pair_in_term hol_ctxt def
@@ -1419,13 +1418,13 @@
       #> destroy_existential_equalities hol_ctxt
       #> simplify_constrs_and_sels thy
       #> distribute_quantifiers
-      #> push_quantifiers_inward thy
+      #> push_quantifiers_inward
       #> close_form
       #> Term.map_abs_vars shortest_name
   in
-    (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
+    (((map (do_rest true) def_ts, map (do_rest false) nondef_ts),
       (got_all_mono_user_axioms, no_poly_user_axioms)),
-     do_rest false true core_t, binarize)
+     do_rest false core_t, binarize)
   end
 
 end;
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_rep.ML
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -166,7 +166,7 @@
 
 (* rep -> rep list *)
 fun binder_reps (Func (R1, R2)) = R1 :: binder_reps R2
-  | binder_reps R = []
+  | binder_reps _ = []
 (* rep -> rep *)
 fun body_rep (Func (_, R2)) = body_rep R2
   | body_rep R = R
@@ -272,10 +272,10 @@
     (case (best_one_rep_for_type scope T1, best_one_rep_for_type scope T2) of
        (Unit, Unit) => Unit
      | (R1, R2) => Struct [R1, R2])
-  | best_one_rep_for_type (scope as {card_assigns, datatypes, ofs, ...}) T =
+  | best_one_rep_for_type {card_assigns, datatypes, ofs, ...} T =
     (case card_of_type card_assigns T of
        1 => if is_some (datatype_spec datatypes T) orelse
-               is_fp_iterator_type T then
+               is_iterator_type T then
               Atom (1, offset_of_type ofs T)
             else
               Unit
@@ -332,7 +332,7 @@
   | type_schema_of_rep (Type ("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 T R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
+  | type_schema_of_rep _ R = raise REP ("Nitpick_Rep.type_schema_of_rep", [R])
 (* typ list -> rep list -> typ list *)
 and type_schema_of_reps Ts Rs = flat (map2 type_schema_of_rep Ts Rs)
 
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -136,7 +136,7 @@
 (* (string -> string) -> scope
    -> string list * string list * string list * string list * string list *)
 fun quintuple_for_scope quote
-        ({hol_ctxt as {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
+        ({hol_ctxt = {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
          datatypes, ...} : scope) =
   let
     val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
@@ -346,7 +346,7 @@
   let
     (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
     fun aux seen [] = SOME seen
-      | aux seen ((T, 0) :: _) = NONE
+      | aux _ ((_, 0) :: _) = NONE
       | aux seen ((T, k) :: rest) =
         (if is_surely_inconsistent_scope_description hol_ctxt binarize
                 ((T, k) :: seen) rest max_assigns then
@@ -359,7 +359,7 @@
   in aux [] (rev card_assigns) end
 
 (* theory -> (typ * int) list -> typ * int -> typ * int *)
-fun repair_iterator_assign thy assigns (T as Type (s, Ts), k) =
+fun repair_iterator_assign thy assigns (T as Type (_, Ts), k) =
     (T, if T = @{typ bisim_iterator} then
           let
             val co_cards = map snd (filter (is_codatatype thy o fst) assigns)
@@ -394,15 +394,15 @@
   end
   handle Option.Option => NONE
 
-(* theory -> (typ * int) list -> dtype_spec list -> int Typtab.table *)
-fun offset_table_for_card_assigns thy assigns dtypes =
+(* (typ * int) list -> dtype_spec list -> int Typtab.table *)
+fun offset_table_for_card_assigns assigns dtypes =
   let
     (* int -> (int * int) list -> (typ * int) list -> int Typtab.table
        -> int Typtab.table *)
     fun aux next _ [] = Typtab.update_new (dummyT, next)
       | aux next reusable ((T, k) :: assigns) =
-        if k = 1 orelse is_fp_iterator_type T orelse is_integer_type T
-           orelse T = @{typ bisim_iterator} orelse is_bit_type T then
+        if k = 1 orelse is_iterator_type T orelse is_integer_type T
+           orelse is_bit_type T then
           aux next reusable assigns
         else if length (these (Option.map #constrs (datatype_spec dtypes T)))
                 > 1 then
@@ -421,12 +421,10 @@
 (* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp
    -> constr_spec list -> constr_spec list *)
 fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards
-                    num_self_recs num_non_self_recs (self_rec, x as (s, T))
+                    num_self_recs num_non_self_recs (self_rec, x as (_, T))
                     constrs =
   let
     val max = constr_max max_assigns x
-    (* int -> int *)
-    fun bound k = Int.min (card, (max >= 0 ? curry Int.min max) k)
     (* unit -> int *)
     fun next_delta () = if null constrs then 0 else #epsilon (hd constrs)
     val {delta, epsilon, exclusive, total} =
@@ -496,14 +494,6 @@
      concrete = concrete, deep = deep, constrs = constrs}
   end
 
-(* int -> int *)
-fun min_bits_for_nat_value n = if n <= 0 then 0 else IntInf.log2 n + 1
-(* scope_desc -> int *)
-fun min_bits_for_max_assigns (_, []) = 0
-  | min_bits_for_max_assigns (card_assigns, max_assigns) =
-    min_bits_for_nat_value (fold Integer.max
-        (map snd card_assigns @ map snd max_assigns) 0)
-
 (* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
 fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break
                           deep_dataTs (desc as (card_assigns, _)) =
@@ -520,7 +510,7 @@
     {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
      datatypes = datatypes, bits = bits, bisim_depth = bisim_depth,
      ofs = if sym_break <= 0 then Typtab.empty
-           else offset_table_for_card_assigns thy card_assigns datatypes}
+           else offset_table_for_card_assigns card_assigns datatypes}
   end
 
 (* theory -> typ list -> (typ option * int list) list
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_tests.ML
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -308,7 +308,7 @@
                        NameTable.empty
     val u = Op1 (Not, type_of u, rep_of u, u)
             |> rename_vars_in_nut pool table
-    val formula = kodkod_formula_from_nut bits Typtab.empty constrs u
+    val formula = kodkod_formula_from_nut Typtab.empty constrs u
     val bounds = map (bound_for_plain_rel ctxt debug) free_rels
     val univ_card = univ_card nat_card int_card j0 bounds formula
     val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)
diff -r 4f6760122b2a -r 54ab4921f826 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Feb 22 10:28:49 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Feb 22 11:57:33 2010 +0100
@@ -92,7 +92,7 @@
 val max_exponent = 16384
 
 (* int -> int -> int *)
-fun reasonable_power a 0 = 1
+fun reasonable_power _ 0 = 1
   | reasonable_power a 1 = a
   | reasonable_power 0 _ = 0
   | reasonable_power 1 _ = 1