# HG changeset patch
# User blanchet
# Date 1266515287 -3600
# Node ID 2bcdae5f4fdb8bee04f507d0c33c268922a83255
# Parent  15a5f213ef5b5d603fef04cc9cb53a222781b5b2
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s

diff -r 15a5f213ef5b -r 2bcdae5f4fdb doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Thu Feb 18 10:38:37 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Thu Feb 18 18:48:07 2010 +0100
@@ -472,7 +472,7 @@
 \prew
 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
 \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
-\slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported
+\slshape Warning: The conjecture either trivially holds for the given scopes or (more likely) lies outside Nitpick's supported
 fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
 Nitpick found a potential counterexample: \\[2\smallskipamount]
 \hbox{}\qquad Free variable: \nopagebreak \\
@@ -2083,7 +2083,6 @@
 Specifies whether the given (recursive) datatype should be given standard
 models. Nonstandard models are unsound but can help debug structural induction
 proofs, as explained in \S\ref{inductive-properties}.
-%This option is not supported for the type \textit{nat}.
 
 \optrue{std}{non\_std}
 Specifies the default standardness to use. This can be overridden on a per-type
diff -r 15a5f213ef5b -r 2bcdae5f4fdb src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Nitpick.thy	Thu Feb 18 18:48:07 2010 +0100
@@ -217,21 +217,6 @@
 definition of_frac :: "'a \<Rightarrow> 'b\<Colon>{inverse,ring_1}" where
 "of_frac q \<equiv> of_int (num q) / of_int (denom q)"
 
-(* While Nitpick normally avoids to unfold definitions for locales, it
-   unfortunately needs to unfold them when dealing with the following built-in
-   constants. A cleaner approach would be to change "Nitpick_HOL" and
-   "Nitpick_Nut" so that they handle the unexpanded overloaded constants
-   directly, but this is slightly more tricky to implement. *)
-lemmas [nitpick_def] = div_int_inst.div_int div_int_inst.mod_int
-    div_nat_inst.div_nat div_nat_inst.mod_nat semilattice_inf_fun_inst.inf_fun
-    minus_fun_inst.minus_fun minus_int_inst.minus_int minus_nat_inst.minus_nat
-    one_int_inst.one_int one_nat_inst.one_nat ord_fun_inst.less_eq_fun
-    ord_int_inst.less_eq_int ord_int_inst.less_int ord_nat_inst.less_eq_nat
-    ord_nat_inst.less_nat plus_int_inst.plus_int plus_nat_inst.plus_nat
-    times_int_inst.times_int times_nat_inst.times_nat uminus_int_inst.uminus_int
-    semilattice_sup_fun_inst.sup_fun zero_int_inst.zero_int
-    zero_nat_inst.zero_nat
-
 use "Tools/Nitpick/kodkod.ML"
 use "Tools/Nitpick/kodkod_sat.ML"
 use "Tools/Nitpick/nitpick_util.ML"
diff -r 15a5f213ef5b -r 2bcdae5f4fdb src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 18 18:48:07 2010 +0100
@@ -265,7 +265,7 @@
                      orig_assm_ts
 *)
     val max_bisim_depth = fold Integer.max bisim_depths ~1
-    val case_names = case_const_names thy
+    val case_names = case_const_names thy stds
     val (defs, built_in_nondefs, user_nondefs) = all_axioms_of thy
     val def_table = const_def_table ctxt defs
     val nondef_table = const_nondef_table (built_in_nondefs @ user_nondefs)
@@ -337,7 +337,7 @@
     val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
     (* typ -> bool *)
     fun is_type_always_monotonic T =
-      (is_datatype thy T andalso not (is_quot_type thy T) andalso
+      (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
        (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
       is_number_type thy T orelse is_bit_type T
     fun is_type_monotonic T =
@@ -347,8 +347,8 @@
       | _ => is_type_always_monotonic T orelse
              formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t
     fun is_deep_datatype T =
-      is_datatype thy T andalso
-      (not standard orelse is_word_type T orelse
+      is_datatype thy stds T andalso
+      (not standard orelse T = nat_T orelse is_word_type T orelse
        exists (curry (op =) T o domain_type o type_of) sel_names)
     val all_Ts = ground_types_in_terms hol_ctxt binarize
                                        (core_t :: def_ts @ nondef_ts)
@@ -519,8 +519,9 @@
           declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk
                                            rel_table datatypes
         val declarative_axioms = plain_axioms @ dtype_axioms
-        val univ_card = univ_card nat_card int_card main_j0
-                                  (plain_bounds @ sel_bounds) formula
+        val univ_card = Int.max (univ_card nat_card int_card main_j0
+                                     (plain_bounds @ sel_bounds) formula,
+                                 main_j0 |> bits > 0 ? Integer.add (bits + 1))
         val built_in_bounds = bounds_for_built_in_rels_in_formula debug
                                   univ_card nat_card int_card main_j0 formula
         val bounds = built_in_bounds @ plain_bounds @ sel_bounds
@@ -837,8 +838,9 @@
                  forall (KK.is_problem_trivially_false o fst)
                         sound_problems then
                 print_m (fn () =>
-                    "Warning: The conjecture either trivially holds or (more \
-                    \likely) lies outside Nitpick's supported fragment." ^
+                    "Warning: The conjecture either trivially holds for the \
+                    \given scopes or (more likely) lies outside Nitpick's \
+                    \supported fragment." ^
                     (if exists (not o KK.is_problem_trivially_false o fst)
                                unsound_problems then
                        " Only potential counterexamples may be found."
diff -r 15a5f213ef5b -r 2bcdae5f4fdb src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 18 18:48:07 2010 +0100
@@ -85,6 +85,7 @@
   val is_integer_type : typ -> bool
   val is_bit_type : typ -> bool
   val is_word_type : typ -> bool
+  val is_integer_like_type : typ -> bool
   val is_record_type : typ -> bool
   val is_number_type : theory -> typ -> bool
   val const_for_iterator_type : typ -> styp
@@ -95,14 +96,13 @@
   val curried_binder_types : typ -> typ list
   val mk_flat_tuple : typ -> term list -> term
   val dest_n_tuple : int -> term -> term list
-  val instantiate_type : theory -> typ -> typ -> typ -> typ
   val is_real_datatype : theory -> string -> bool
-  val is_standard_datatype : hol_context -> typ -> bool
+  val is_standard_datatype : theory -> (typ option * bool) list -> typ -> bool
   val is_quot_type : theory -> typ -> bool
   val is_codatatype : theory -> typ -> bool
   val is_pure_typedef : theory -> typ -> bool
   val is_univ_typedef : theory -> typ -> bool
-  val is_datatype : theory -> typ -> bool
+  val is_datatype : theory -> (typ option * bool) list -> typ -> bool
   val is_record_constr : styp -> bool
   val is_record_get : theory -> styp -> bool
   val is_record_update : theory -> styp -> bool
@@ -113,7 +113,7 @@
   val mate_of_rep_fun : theory -> styp -> styp
   val is_constr_like : theory -> styp -> bool
   val is_stale_constr : theory -> styp -> bool
-  val is_constr : theory -> styp -> bool
+  val is_constr : theory -> (typ option * bool) list -> styp -> bool
   val is_sel : string -> bool
   val is_sel_like_and_no_discr : string -> bool
   val box_type : hol_context -> boxability -> typ -> typ
@@ -141,8 +141,10 @@
   val constr_name_for_sel_like : string -> string
   val binarized_and_boxed_constr_for_sel : hol_context -> bool -> styp -> styp
   val discriminate_value : hol_context -> styp -> term -> term
-  val select_nth_constr_arg : theory -> styp -> term -> int -> typ -> term
-  val construct_value : theory -> styp -> term list -> term
+  val select_nth_constr_arg :
+    theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term
+  val construct_value :
+    theory -> (typ option * bool) list -> styp -> term list -> term
   val card_of_type : (typ * int) list -> typ -> int
   val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
   val bounded_exact_card_of_type :
@@ -151,10 +153,13 @@
   val special_bounds : term list -> (indexname * typ) list
   val is_funky_typedef : theory -> typ -> bool
   val all_axioms_of : theory -> term list * term list * term list
-  val arity_of_built_in_const : bool -> styp -> int option
-  val is_built_in_const : bool -> styp -> bool
+  val arity_of_built_in_const :
+    theory -> (typ option * bool) list -> bool -> styp -> int option
+  val is_built_in_const :
+    theory -> (typ option * bool) list -> bool -> styp -> bool
   val term_under_def : term -> term
-  val case_const_names : theory -> (string * int) list
+  val case_const_names :
+    theory -> (typ option * bool) list -> (string * int) list
   val const_def_table : Proof.context -> term list -> const_table
   val const_nondef_table : term list -> const_table
   val const_simp_table : Proof.context -> const_table
@@ -165,7 +170,8 @@
   val add_simps : const_table Unsynchronized.ref -> string -> term list -> unit
   val inverse_axioms_for_rep_fun : theory -> styp -> term list
   val optimized_typedef_axioms : theory -> string * typ list -> term list
-  val optimized_quot_type_axioms : theory -> string * typ list -> term list
+  val optimized_quot_type_axioms :
+    theory -> (typ option * bool) list -> string * typ list -> term list
   val def_of_const : theory -> const_table -> styp -> term option
   val fixpoint_kind_of_const :
     theory -> const_table -> string * typ -> fixpoint_kind
@@ -340,44 +346,45 @@
    (@{const_name trancl}, 1),
    (@{const_name rel_comp}, 2),
    (@{const_name image}, 2),
-   (@{const_name Suc}, 0),
    (@{const_name finite}, 1),
-   (@{const_name nat}, 0),
-   (@{const_name zero_nat_inst.zero_nat}, 0),
-   (@{const_name one_nat_inst.one_nat}, 0),
-   (@{const_name plus_nat_inst.plus_nat}, 0),
-   (@{const_name minus_nat_inst.minus_nat}, 0),
-   (@{const_name times_nat_inst.times_nat}, 0),
-   (@{const_name div_nat_inst.div_nat}, 0),
-   (@{const_name ord_nat_inst.less_nat}, 2),
-   (@{const_name ord_nat_inst.less_eq_nat}, 2),
-   (@{const_name nat_gcd}, 0),
-   (@{const_name nat_lcm}, 0),
-   (@{const_name zero_int_inst.zero_int}, 0),
-   (@{const_name one_int_inst.one_int}, 0),
-   (@{const_name plus_int_inst.plus_int}, 0),
-   (@{const_name minus_int_inst.minus_int}, 0),
-   (@{const_name times_int_inst.times_int}, 0),
-   (@{const_name div_int_inst.div_int}, 0),
-   (@{const_name uminus_int_inst.uminus_int}, 0),
-   (@{const_name ord_int_inst.less_int}, 2),
-   (@{const_name ord_int_inst.less_eq_int}, 2),
    (@{const_name unknown}, 0),
    (@{const_name is_unknown}, 1),
    (@{const_name Tha}, 1),
    (@{const_name Frac}, 0),
    (@{const_name norm_frac}, 0)]
+val built_in_nat_consts =
+  [(@{const_name Suc}, 0),
+   (@{const_name nat}, 0),
+   (@{const_name nat_gcd}, 0),
+   (@{const_name nat_lcm}, 0)]
 val built_in_descr_consts =
   [(@{const_name The}, 1),
    (@{const_name Eps}, 1)]
 val built_in_typed_consts =
-  [((@{const_name of_nat}, nat_T --> int_T), 0),
-   ((@{const_name of_nat}, @{typ "unsigned_bit word => signed_bit word"}), 0)]
+  [((@{const_name zero_class.zero}, int_T), 0),
+   ((@{const_name one_class.one}, int_T), 0),
+   ((@{const_name plus_class.plus}, int_T --> int_T --> int_T), 0),
+   ((@{const_name minus_class.minus}, int_T --> int_T --> int_T), 0),
+   ((@{const_name times_class.times}, int_T --> int_T --> int_T), 0),
+   ((@{const_name div_class.div}, int_T --> int_T --> int_T), 0),
+   ((@{const_name uminus_class.uminus}, int_T --> int_T), 0),
+   ((@{const_name ord_class.less}, int_T --> int_T --> bool_T), 2),
+   ((@{const_name ord_class.less_eq}, int_T --> int_T --> bool_T), 2)]
+val built_in_typed_nat_consts =
+  [((@{const_name zero_class.zero}, nat_T), 0),
+   ((@{const_name one_class.one}, nat_T), 0),
+   ((@{const_name plus_class.plus}, nat_T --> nat_T --> nat_T), 0),
+   ((@{const_name minus_class.minus}, nat_T --> nat_T --> nat_T), 0),
+   ((@{const_name times_class.times}, nat_T --> nat_T --> nat_T), 0),
+   ((@{const_name div_class.div}, nat_T --> nat_T --> nat_T), 0),
+   ((@{const_name ord_class.less}, nat_T --> nat_T --> bool_T), 2),
+   ((@{const_name ord_class.less_eq}, nat_T --> nat_T --> bool_T), 2),
+   ((@{const_name of_nat}, nat_T --> int_T), 0)]
 val built_in_set_consts =
-  [(@{const_name semilattice_inf_fun_inst.inf_fun}, 2),
-   (@{const_name semilattice_sup_fun_inst.sup_fun}, 2),
-   (@{const_name minus_fun_inst.minus_fun}, 2),
-   (@{const_name ord_fun_inst.less_eq_fun}, 2)]
+  [(@{const_name semilattice_inf_class.inf}, 2),
+   (@{const_name semilattice_sup_class.sup}, 2),
+   (@{const_name minus_class.minus}, 2),
+   (@{const_name ord_class.less_eq}, 2)]
 
 (* typ -> typ *)
 fun unarize_type @{typ "unsigned_bit word"} = nat_T
@@ -449,17 +456,19 @@
   | is_gfp_iterator_type _ = false
 val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
 fun is_boolean_type T = (T = prop_T orelse T = bool_T)
-val is_integer_type =
-  member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
+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_record_type = not o null o Record.dest_recTs
 (* theory -> typ -> bool *)
 fun is_frac_type thy (Type (s, [])) =
     not (null (these (AList.lookup (op =) (#frac_types (Data.get thy)) s)))
   | is_frac_type _ _ = false
-fun is_number_type thy = is_integer_type orf is_frac_type thy
+fun is_number_type thy = is_integer_like_type orf is_frac_type thy
 
 (* bool -> styp -> typ *)
 fun iterator_type_for_const gfp (s, T) =
@@ -507,13 +516,41 @@
   | dest_n_tuple_type _ T =
     raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
 
+type typedef_info =
+  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
+   set_def: thm option, prop_of_Rep: thm, set_name: string,
+   Abs_inverse: thm option, Rep_inverse: thm option}
+
+(* theory -> string -> typedef_info *)
+fun typedef_info thy s =
+  if is_frac_type thy (Type (s, [])) then
+    SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
+          Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
+          set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
+                          |> Logic.varify,
+          set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
+  else case Typedef.get_info thy s of
+    SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
+          Rep_inverse, ...} =>
+    SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
+          Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
+          set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
+          Rep_inverse = SOME Rep_inverse}
+  | NONE => NONE
+
+(* theory -> string -> bool *)
+val is_typedef = is_some oo typedef_info
+val is_real_datatype = is_some oo Datatype.get_info
+(* theory -> (typ option * bool) list -> typ -> bool *)
+fun is_standard_datatype thy = the oo triple_lookup (type_match thy)
+
 (* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
    e.g., by adding a field to "Datatype_Aux.info". *)
-(* string -> bool *)
-val is_basic_datatype =
-    member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
-                   @{type_name nat}, @{type_name int},
-                   "Code_Numeral.code_numeral"]
+(* theory -> (typ option * bool) list -> string -> bool *)
+fun is_basic_datatype thy stds s =
+  member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
+                 @{type_name int}, "Code_Numeral.code_numeral"] s orelse
+  (s = @{type_name nat} andalso is_standard_datatype thy stds nat_T)
 
 (* theory -> typ -> typ -> typ -> typ *)
 fun instantiate_type thy T1 T1' T2 =
@@ -544,7 +581,8 @@
     val (co_s, co_Ts) = dest_Type co_T
     val _ =
       if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
-         co_s <> "fun" andalso not (is_basic_datatype co_s) then
+         co_s <> "fun" andalso
+         not (is_basic_datatype thy [(NONE, true)] co_s) then
         ()
       else
         raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
@@ -554,35 +592,6 @@
 (* typ -> theory -> theory *)
 fun unregister_codatatype co_T = register_codatatype co_T "" []
 
-type typedef_info =
-  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
-   set_def: thm option, prop_of_Rep: thm, set_name: string,
-   Abs_inverse: thm option, Rep_inverse: thm option}
-
-(* theory -> string -> typedef_info *)
-fun typedef_info thy s =
-  if is_frac_type thy (Type (s, [])) then
-    SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
-          Abs_name = @{const_name Abs_Frac}, Rep_name = @{const_name Rep_Frac},
-          set_def = NONE, prop_of_Rep = @{prop "Rep_Frac x \<in> Frac"}
-                          |> Logic.varify,
-          set_name = @{const_name Frac}, Abs_inverse = NONE, Rep_inverse = NONE}
-  else case Typedef.get_info thy s of
-    SOME {abs_type, rep_type, Abs_name, Rep_name, set_def, Rep, Abs_inverse,
-          Rep_inverse, ...} =>
-    SOME {abs_type = abs_type, rep_type = rep_type, Abs_name = Abs_name,
-          Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
-          set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
-          Rep_inverse = SOME Rep_inverse}
-  | NONE => NONE
-
-(* theory -> string -> bool *)
-val is_typedef = is_some oo typedef_info
-val is_real_datatype = is_some oo Datatype.get_info
-(* hol_context -> typ -> bool *)
-fun is_standard_datatype ({thy, stds, ...} : hol_context) =
-  the o triple_lookup (type_match thy) stds
-
 (* theory -> typ -> bool *)
 fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
   | is_quot_type _ (Type ("FSet.fset", _)) = true
@@ -594,7 +603,8 @@
 fun is_pure_typedef thy (T as Type (s, _)) =
     is_typedef thy s andalso
     not (is_real_datatype thy s orelse is_quot_type thy T orelse
-         is_codatatype thy T orelse is_record_type T orelse is_integer_type T)
+         is_codatatype thy T orelse is_record_type T orelse
+         is_integer_like_type T)
   | is_pure_typedef _ _ = false
 fun is_univ_typedef thy (Type (s, _)) =
     (case typedef_info thy s of
@@ -607,11 +617,11 @@
                o HOLogic.dest_Trueprop) prop_of_Rep) = SOME @{const_name top}
      | NONE => false)
   | is_univ_typedef _ _ = false
-fun is_datatype thy (T as Type (s, _)) =
+(* theory -> (typ option * bool) list -> typ -> bool *)
+fun is_datatype thy stds (T as Type (s, _)) =
     (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
-     is_quot_type thy T) andalso
-    not (is_basic_datatype s)
-  | is_datatype _ _ = false
+     is_quot_type thy T) andalso not (is_basic_datatype thy stds s)
+  | is_datatype _ _ _ = false
 
 (* theory -> typ -> (string * typ) list * (string * typ) *)
 fun all_record_fields thy T =
@@ -699,15 +709,16 @@
   let val (x as (s, T)) = (s, unarize_and_unbox_type T) in
     Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
     (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
-    x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
     is_coconstr thy x
   end
 fun is_stale_constr thy (x as (_, T)) =
   is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
   not (is_coconstr thy x)
-fun is_constr thy (x as (_, T)) =
+(* theory -> (typ option * bool) list -> styp -> bool *)
+fun is_constr thy stds (x as (_, T)) =
   is_constr_like thy x andalso
-  not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
+  not (is_basic_datatype thy stds
+                         (fst (dest_Type (unarize_type (body_type T))))) andalso
   not (is_stale_constr thy x)
 (* string -> bool *)
 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
@@ -844,15 +855,16 @@
   #> List.foldr (s_conj o swap) @{const True}
 
 (* typ -> term *)
-fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
+fun zero_const T = Const (@{const_name zero_class.zero}, T)
 fun suc_const T = Const (@{const_name Suc}, T --> T)
 
-(* theory -> typ -> styp list *)
-fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
+(* hol_context -> typ -> styp list *)
+fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
+                              (T as Type (s, Ts)) =
     (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
        SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
      | _ =>
-       if is_datatype thy T then
+       if is_datatype thy stds T then
          case Datatype.get_info thy s of
            SOME {index, descr, ...} =>
            let
@@ -883,11 +895,11 @@
          [])
   | uncached_datatype_constrs _ _ = []
 (* hol_context -> typ -> styp list *)
-fun datatype_constrs ({thy, constr_cache, ...} : hol_context) T =
+fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
   case AList.lookup (op =) (!constr_cache) T of
     SOME xs => xs
   | NONE =>
-    let val xs = uncached_datatype_constrs thy T in
+    let val xs = uncached_datatype_constrs hol_ctxt T in
       (Unsynchronized.change constr_cache (cons (T, xs)); xs)
     end
 (* hol_context -> bool -> typ -> styp list *)
@@ -930,11 +942,11 @@
     else betapply (discr_term_for_constr hol_ctxt x, t)
   | _ => betapply (discr_term_for_constr hol_ctxt x, t)
 
-(* styp -> term -> term *)
-fun nth_arg_sel_term_for_constr (x as (s, T)) n =
+(* theory -> (typ option * bool) list -> styp -> term -> term *)
+fun nth_arg_sel_term_for_constr thy stds (x as (s, T)) n =
   let val (arg_Ts, dataT) = strip_type T in
-    if dataT = nat_T then
-      @{term "%n::nat. minus_nat_inst.minus_nat n one_nat_inst.one_nat"}
+    if dataT = nat_T andalso is_standard_datatype thy stds nat_T then
+      @{term "%n::nat. n - 1"}
     else if is_pair_type dataT then
       Const (nth_sel_for_constr x n)
     else
@@ -952,24 +964,26 @@
                      (List.take (arg_Ts, n)) 0
       in Abs ("x", dataT, aux m (nth arg_Ts n) |> snd) end
   end
-(* theory -> styp -> term -> int -> typ -> term *)
-fun select_nth_constr_arg thy x t n res_T =
-  case strip_comb t of
-    (Const x', args) =>
-    if x = x' then nth args n
-    else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
-    else betapply (nth_arg_sel_term_for_constr x n, t)
-  | _ => betapply (nth_arg_sel_term_for_constr x n, t)
+(* theory -> (typ option * bool) list -> styp -> term -> int -> typ -> term *)
+fun select_nth_constr_arg thy stds x t n res_T =
+  (case strip_comb t of
+     (Const x', args) =>
+     if x = x' then nth args n
+     else if is_constr_like thy x' then Const (@{const_name unknown}, res_T)
+     else raise SAME ()
+   | _ => raise SAME())
+  handle SAME () => betapply (nth_arg_sel_term_for_constr thy stds x n, t)
 
-(* theory -> styp -> term list -> term *)
-fun construct_value _ x [] = Const x
-  | construct_value thy (x as (s, _)) args =
+(* theory -> (typ option * bool) list -> styp -> term list -> term *)
+fun construct_value _ _ x [] = Const x
+  | 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 =>
         if is_sel_like_and_no_discr s' andalso
            constr_name_for_sel_like s' = s andalso
-           forall (fn (n, t') => select_nth_constr_arg thy x t n dummyT = t')
+           forall (fn (n, t') =>
+                      select_nth_constr_arg thy stds x t n dummyT = t')
                   (index_seq 0 (length args) ~~ args) then
           t
         else
@@ -1167,24 +1181,31 @@
       user_defs @ built_in_defs
   in (defs, built_in_nondefs, user_nondefs) end
 
-(* bool -> styp -> int option *)
-fun arity_of_built_in_const fast_descrs (s, T) =
+(* theory -> (typ option * bool) list -> bool -> styp -> int option *)
+fun arity_of_built_in_const thy stds fast_descrs (s, T) =
   if s = @{const_name If} then
     if nth_range_type 3 T = @{typ bool} then NONE else SOME 3
-  else case AList.lookup (op =)
-                (built_in_consts
-                 |> fast_descrs ? append built_in_descr_consts) s of
-    SOME n => SOME n
-  | NONE =>
-    case AList.lookup (op =) built_in_typed_consts (s, 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
-(* bool -> styp -> bool *)
-val is_built_in_const = is_some oo arity_of_built_in_const
+  else
+    let val std_nats = is_standard_datatype thy stds nat_T in
+      case AList.lookup (op =)
+                    (built_in_consts
+                     |> std_nats ? append built_in_nat_consts
+                     |> fast_descrs ? append built_in_descr_consts) s of
+        SOME n => SOME n
+      | NONE =>
+        case AList.lookup (op =)
+                 (built_in_typed_consts
+                  |> std_nats ? append built_in_typed_nat_consts)
+                 (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
+    end
+(* theory -> (typ option * bool) list -> bool -> styp -> bool *)
+val is_built_in_const = is_some oooo arity_of_built_in_const
 
 (* This function is designed to work for both real definition axioms and
    simplification rules (equational specifications). *)
@@ -1202,9 +1223,10 @@
 (* Here we crucially rely on "Refute.specialize_type" performing a preorder
    traversal of the term, without which the wrong occurrence of a constant could
    be matched in the face of overloading. *)
-(* theory -> bool -> const_table -> styp -> term list *)
-fun def_props_for_const thy fast_descrs table (x as (s, _)) =
-  if is_built_in_const fast_descrs x then
+(* theory -> (typ option * bool) list -> bool -> const_table -> styp
+   -> term list *)
+fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
+  if is_built_in_const thy stds fast_descrs x then
     []
   else
     these (Symtab.lookup table s)
@@ -1229,10 +1251,11 @@
 
 (* theory -> const_table -> styp -> term option *)
 fun def_of_const thy table (x as (s, _)) =
-  if is_built_in_const false x orelse original_name s <> s then
+  if is_built_in_const thy [(NONE, false)] false x orelse
+     original_name s <> s then
     NONE
   else
-    x |> def_props_for_const thy false table |> List.last
+    x |> def_props_for_const thy [(NONE, false)] false table |> List.last
       |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
     handle List.Empty => NONE
 
@@ -1282,10 +1305,10 @@
 fun table_for get ctxt =
   get ctxt |> map pair_for_prop |> AList.group (op =) |> Symtab.make
 
-(* theory -> (string * int) list *)
-fun case_const_names thy =
+(* theory -> (typ option * bool) list -> (string * int) list *)
+fun case_const_names thy stds =
   Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
-                  if is_basic_datatype dtype_s then
+                  if is_basic_datatype thy stds dtype_s then
                     I
                   else
                     cons (case_name, AList.lookup (op =) descr index
@@ -1366,7 +1389,7 @@
       end
     | NONE => []
   end
-fun optimized_quot_type_axioms thy abs_z =
+fun optimized_quot_type_axioms thy stds abs_z =
   let
     val abs_T = Type abs_z
     val rep_T = rep_type_for_quot_type thy abs_T
@@ -1375,7 +1398,7 @@
     val x_var = Var (("x", 0), rep_T)
     val y_var = Var (("y", 0), rep_T)
     val x = (@{const_name Quot}, rep_T --> abs_T)
-    val sel_a_t = select_nth_constr_arg thy x a_var 0 rep_T
+    val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
     val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T)
     val normal_x = normal_t $ x_var
     val normal_y = normal_t $ y_var
@@ -1392,31 +1415,31 @@
          $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
   end
 
-(* theory -> int * styp -> term *)
-fun constr_case_body thy (j, (x as (_, T))) =
+(* theory -> (typ option * bool) list -> int * styp -> term *)
+fun constr_case_body thy stds (j, (x as (_, T))) =
   let val arg_Ts = binder_types T in
-    list_comb (Bound j, map2 (select_nth_constr_arg thy x (Bound 0))
+    list_comb (Bound j, map2 (select_nth_constr_arg thy stds x (Bound 0))
                              (index_seq 0 (length arg_Ts)) arg_Ts)
   end
 (* hol_context -> typ -> int * styp -> term -> term *)
-fun add_constr_case (hol_ctxt as {thy, ...}) res_T (j, x) res_t =
+fun add_constr_case (hol_ctxt as {thy, stds, ...}) res_T (j, x) res_t =
   Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
-  $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy (j, x)
+  $ discriminate_value hol_ctxt x (Bound 0) $ constr_case_body thy stds (j, x)
   $ res_t
 (* hol_context -> typ -> typ -> term *)
-fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
+fun optimized_case_def (hol_ctxt as {thy, stds, ...}) dataT res_T =
   let
     val xs = datatype_constrs hol_ctxt dataT
     val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
     val (xs', x) = split_last xs
   in
-    constr_case_body thy (1, x)
+    constr_case_body thy stds (1, x)
     |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
     |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   end
 
 (* hol_context -> string -> typ -> typ -> term -> term *)
-fun optimized_record_get (hol_ctxt as {thy, ...}) s rec_T res_T t =
+fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t =
   let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
     case no_of_record_field thy s rec_T of
       ~1 => (case rec_T of
@@ -1425,65 +1448,56 @@
                  val rec_T' = List.last Ts
                  val j = num_record_fields thy rec_T - 1
                in
-                 select_nth_constr_arg thy constr_x t j res_T
+                 select_nth_constr_arg thy stds constr_x t j res_T
                  |> optimized_record_get hol_ctxt s rec_T' res_T
                end
              | _ => raise TYPE ("Nitpick_HOL.optimized_record_get", [rec_T],
                                 []))
-    | j => select_nth_constr_arg thy constr_x t j res_T
+    | j => select_nth_constr_arg thy stds constr_x t j res_T
   end
 (* hol_context -> string -> typ -> term -> term -> term *)
-fun optimized_record_update (hol_ctxt as {thy, ...}) s rec_T fun_t rec_t =
+fun optimized_record_update (hol_ctxt as {thy, stds, ...}) s rec_T fun_t rec_t =
   let
     val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
     val Ts = binder_types constr_T
     val n = length Ts
     val special_j = no_of_record_field thy s rec_T
-    val ts = map2 (fn j => fn T =>
-                      let
-                        val t = select_nth_constr_arg thy constr_x rec_t j T
-                      in
-                        if j = special_j then
-                          betapply (fun_t, t)
-                        else if j = n - 1 andalso special_j = ~1 then
-                          optimized_record_update hol_ctxt s
-                              (rec_T |> dest_Type |> snd |> List.last) fun_t t
-                        else
-                          t
-                      end) (index_seq 0 n) Ts
+    val ts =
+      map2 (fn j => fn T =>
+               let val t = select_nth_constr_arg thy stds constr_x rec_t j T in
+                 if j = special_j then
+                   betapply (fun_t, t)
+                 else if j = n - 1 andalso special_j = ~1 then
+                   optimized_record_update hol_ctxt s
+                       (rec_T |> dest_Type |> snd |> List.last) fun_t t
+                 else
+                   t
+               end) (index_seq 0 n) Ts
   in list_comb (Const constr_x, ts) end
 
-(* Constants "c" whose definition is of the form "c == c'", where "c'" is also a
-   constant, are said to be trivial. For those, we ignore the simplification
-   rules and use the definition instead, to ensure that built-in symbols like
-   "ord_nat_inst.less_eq_nat" are picked up correctly. *)
-(* theory -> const_table -> styp -> bool *)
-fun has_trivial_definition thy table x =
-  case def_of_const thy table x of SOME (Const _) => true | _ => false
-
 (* theory -> const_table -> string * typ -> fixpoint_kind *)
 fun fixpoint_kind_of_const thy table x =
-  if is_built_in_const false x then
+  if is_built_in_const thy [(NONE, false)] false x then
     NoFp
   else
     fixpoint_kind_of_rhs (the (def_of_const thy table x))
     handle Option.Option => NoFp
 
 (* hol_context -> styp -> bool *)
-fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
-                            : hol_context) x =
-  not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
-  fixpoint_kind_of_const thy def_table x <> NoFp
-fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
-                            : hol_context) x =
-  exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
+fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table,
+                             ...} : hol_context) x =
+  fixpoint_kind_of_const thy def_table x <> NoFp andalso
+  not (null (def_props_for_const thy stds fast_descrs intro_table x))
+fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table,
+                             ...} : hol_context) x =
+  exists (fn table => not (null (def_props_for_const thy stds fast_descrs table
+                                                     x)))
          [!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, ...}) =
   (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)
-  andf (not o has_trivial_definition thy def_table)
 
 (* term * term -> term *)
 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
@@ -1522,7 +1536,7 @@
 val unfold_max_depth = 255
 
 (* hol_context -> term -> term *)
-fun unfold_defs_in_term (hol_ctxt as {thy, destroy_constrs, fast_descrs,
+fun unfold_defs_in_term (hol_ctxt as {thy, stds, destroy_constrs, fast_descrs,
                                       case_names, def_table, ground_thm_table,
                                       ersatz_table, ...}) =
   let
@@ -1537,8 +1551,11 @@
                          |> ran_T = nat_T ? Integer.max 0
               val s = numeral_prefix ^ signed_string_of_int j
             in
-              if is_integer_type ran_T then
-                Const (s, ran_T)
+              if is_integer_like_type ran_T then
+                if is_standard_datatype thy stds ran_T then
+                  Const (s, ran_T)
+                else
+                  funpow j (curry (op $) (suc_const ran_T)) (zero_const ran_T)
               else
                 do_term depth Ts (Const (@{const_name of_int}, int_T --> ran_T)
                                   $ Const (s, int_T))
@@ -1577,9 +1594,9 @@
     (* int -> typ list -> styp -> term list -> int -> typ -> term * term list *)
     and select_nth_constr_arg_with_args _ _ (x as (_, T)) [] n res_T =
         (Abs (Name.uu, body_type T,
-              select_nth_constr_arg thy x (Bound 0) n res_T), [])
+              select_nth_constr_arg thy stds x (Bound 0) n res_T), [])
       | select_nth_constr_arg_with_args depth Ts x (t :: ts) n res_T =
-        (select_nth_constr_arg thy x (do_term depth Ts t) n res_T, ts)
+        (select_nth_constr_arg thy stds x (do_term depth Ts t) n res_T, ts)
     (* int -> typ list -> term -> styp -> term list -> term *)
     and do_const depth Ts t (x as (s, T)) ts =
       case AList.lookup (op =) ersatz_table s of
@@ -1588,7 +1605,7 @@
       | NONE =>
         let
           val (const, ts) =
-            if is_built_in_const fast_descrs x then
+            if is_built_in_const thy stds fast_descrs x then
               (Const x, ts)
             else case AList.lookup (op =) case_names s of
               SOME n =>
@@ -1600,7 +1617,7 @@
                  |> do_term (depth + 1) Ts, ts)
               end
             | _ =>
-              if is_constr thy x then
+              if is_constr thy stds x then
                 (Const x, ts)
               else if is_stale_constr thy x then
                 raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
@@ -1635,7 +1652,7 @@
                 | n => (do_term depth Ts (eta_expand Ts t (2 - n)), [])
               else if is_rep_fun thy x then
                 let val x' = mate_of_rep_fun thy x in
-                  if is_constr thy x' then
+                  if is_constr thy stds x' then
                     select_nth_constr_arg_with_args depth Ts x' ts 0
                                                     (range_type T)
                   else
@@ -1659,7 +1676,7 @@
   in do_term 0 [] end
 
 (* hol_context -> typ -> term list *)
-fun codatatype_bisim_axioms (hol_ctxt as {thy, ...}) T =
+fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T =
   let
     val xs = datatype_constrs hol_ctxt T
     val set_T = T --> bool_T
@@ -1677,8 +1694,8 @@
     fun nth_sub_bisim x n nth_T =
       (if is_codatatype thy nth_T then bisim_const $ n_var_minus_1
        else HOLogic.eq_const nth_T)
-      $ select_nth_constr_arg thy x x_var n nth_T
-      $ select_nth_constr_arg thy x y_var n nth_T
+      $ select_nth_constr_arg thy stds x x_var n nth_T
+      $ select_nth_constr_arg thy stds x y_var n nth_T
     (* styp -> term *)
     fun case_func (x as (_, T)) =
       let
@@ -1695,7 +1712,7 @@
                       map case_func xs @ [x_var]))),
      HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
      $ (Const (@{const_name insert}, T --> set_T --> set_T)
-        $ x_var $ Const (@{const_name bot_fun_inst.bot_fun}, set_T))]
+        $ x_var $ Const (@{const_name bot_class.bot}, set_T))]
     |> map HOLogic.mk_Trueprop
   end
 
@@ -1753,9 +1770,9 @@
 
 (* hol_context -> const_table -> styp -> bool *)
 fun uncached_is_well_founded_inductive_pred
-        ({thy, ctxt, debug, fast_descrs, tac_timeout, intro_table, ...}
+        ({thy, ctxt, stds, debug, fast_descrs, tac_timeout, intro_table, ...}
          : hol_context) (x as (_, T)) =
-  case def_props_for_const thy fast_descrs intro_table x of
+  case def_props_for_const thy stds fast_descrs intro_table x of
     [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
                       [Const x])
   | intro_ts =>
@@ -1999,10 +2016,10 @@
     raw_inductive_pred_axiom hol_ctxt x
 
 (* hol_context -> styp -> term list *)
-fun raw_equational_fun_axioms (hol_ctxt as {thy, fast_descrs, simp_table,
+fun raw_equational_fun_axioms (hol_ctxt as {thy, stds, fast_descrs, simp_table,
                                             psimp_table, ...}) (x as (s, _)) =
-  case def_props_for_const thy fast_descrs (!simp_table) x of
-    [] => (case def_props_for_const thy fast_descrs psimp_table x of
+  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]
            | psimps => psimps)
   | simps => simps
diff -r 15a5f213ef5b -r 2bcdae5f4fdb src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Feb 18 18:48:07 2010 +0100
@@ -131,8 +131,7 @@
   let
     (* int -> int -> int -> KK.int_bound list *)
     fun aux 0  _ _ = []
-      | aux 1 pow_of_two j =
-        if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else []
+      | aux 1 pow_of_two j = [(SOME (~ pow_of_two), [single_atom j])]
       | aux iter pow_of_two j =
         (SOME pow_of_two, [single_atom j]) ::
         aux (iter - 1) (2 * pow_of_two) (j + 1)
diff -r 15a5f213ef5b -r 2bcdae5f4fdb src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Feb 18 18:48:07 2010 +0100
@@ -264,8 +264,8 @@
    -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
    -> typ -> rep -> int list list -> term *)
 fun reconstruct_term unfold pool (maybe_name, base_name, step_name, abs_name)
-        ({hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits, datatypes,
-          ofs, ...} : scope) sel_names rel_table bounds =
+        ({hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns, bits,
+          datatypes, ofs, ...} : scope) sel_names rel_table bounds =
   let
     val for_auto = (maybe_name = "")
     (* int list list -> int *)
@@ -388,7 +388,7 @@
         if j = 0 then @{const False} else @{const True}
       | term_for_atom _ @{typ unit} _ _ _ = @{const Unity}
       | term_for_atom seen T _ j k =
-        if T = nat_T then
+        if T = nat_T andalso is_standard_datatype thy stds nat_T then
           HOLogic.mk_number nat_T j
         else if T = int_T then
           HOLogic.mk_number int_T (int_for_atom (k, 0) j)
@@ -713,7 +713,9 @@
       handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
     val (codatatypes, datatypes) =
       datatypes |> filter #deep |> List.partition #co
-                ||> append (integer_datatype nat_T @ integer_datatype int_T)
+                ||> append (integer_datatype int_T
+                            |> is_standard_datatype thy stds nat_T
+                               ? append (integer_datatype nat_T))
     val block_of_datatypes =
       if show_datatypes andalso not (null datatypes) then
         [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
diff -r 15a5f213ef5b -r 2bcdae5f4fdb src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 18 18:48:07 2010 +0100
@@ -130,7 +130,7 @@
 fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
     could_exist_alpha_subtype alpha_T T
   | could_exist_alpha_sub_ctype thy alpha_T T =
-    (T = alpha_T orelse is_datatype thy T)
+    (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
 
 (* ctype -> bool *)
 fun exists_alpha_sub_ctype CAlpha = true
@@ -545,8 +545,9 @@
   handle List.Empty => initial_gamma
 
 (* cdata -> term -> accumulator -> ctype * accumulator *)
-fun consider_term (cdata as {hol_ctxt as {ctxt, thy, def_table, ...}, alpha_T,
-                             max_fresh, ...}) =
+fun consider_term (cdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
+                                          def_table, ...},
+                             alpha_T, max_fresh, ...}) =
   let
     (* typ -> ctype *)
     val ctype_for = fresh_ctype_for_type cdata
@@ -663,10 +664,6 @@
                 in (CFun (ab_set_C, S Minus, ba_set_C), accum) end
               | @{const_name trancl} => do_fragile_set_operation T accum
               | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)
-              | @{const_name semilattice_inf_fun_inst.inf_fun} =>
-                do_robust_set_operation T accum
-              | @{const_name semilattice_sup_fun_inst.sup_fun} =>
-                do_robust_set_operation T accum
               | @{const_name finite} =>
                 let val C1 = ctype_for (domain_type (domain_type T)) in
                   (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum)
@@ -710,19 +707,6 @@
                   (CFun (a_set_C, S Minus,
                          CFun (a_to_b_set_C, S Minus, ab_set_C)), accum)
                 end
-              | @{const_name minus_fun_inst.minus_fun} =>
-                let
-                  val set_T = domain_type T
-                  val left_set_C = ctype_for set_T
-                  val right_set_C = ctype_for set_T
-                in
-                  (CFun (left_set_C, S Minus,
-                         CFun (right_set_C, S Minus, left_set_C)),
-                   (gamma, cset |> add_ctype_is_right_unique right_set_C
-                                |> add_is_sub_ctype right_set_C left_set_C))
-                end
-              | @{const_name ord_fun_inst.less_eq_fun} =>
-                do_fragile_set_operation T accum
               | @{const_name Tha} =>
                 let
                   val a_C = ctype_for (domain_type (domain_type T))
@@ -732,24 +716,44 @@
                 let val dom_C = ctype_for (domain_type T) in
                   (CFun (dom_C, S Minus, dom_C), accum)
                 end
-              | _ => if is_sel s then
-                       if constr_name_for_sel_like s = @{const_name FunBox} then
-                         let val dom_C = ctype_for (domain_type T) in
-                           (CFun (dom_C, S Minus, dom_C), accum)
-                         end
-                       else
-                         (ctype_for_sel cdata x, accum)
-                     else if is_constr thy x then
-                       (ctype_for_constr cdata x, accum)
-                     else if is_built_in_const true x then
-                       case def_of_const thy def_table x of
-                         SOME t' => do_term t' accum
-                       | NONE => (print_g ("*** built-in " ^ s); unsolvable)
-                     else
-                       let val C = ctype_for T in
-                         (C, ({bounds = bounds, frees = frees,
-                               consts = (x, C) :: consts}, cset))
-                       end)
+              | _ =>
+                if s = @{const_name minus_class.minus} andalso
+                   is_set_type (domain_type T) then
+                  let
+                    val set_T = domain_type T
+                    val left_set_C = ctype_for set_T
+                    val right_set_C = ctype_for set_T
+                  in
+                    (CFun (left_set_C, S Minus,
+                           CFun (right_set_C, S Minus, left_set_C)),
+                     (gamma, cset |> add_ctype_is_right_unique right_set_C
+                                  |> add_is_sub_ctype right_set_C left_set_C))
+                  end
+                else if s = @{const_name ord_class.less_eq} andalso
+                        is_set_type (domain_type T) then
+                  do_fragile_set_operation T accum
+                else if (s = @{const_name semilattice_inf_class.inf} orelse
+                         s = @{const_name semilattice_sup_class.sup}) andalso
+                        is_set_type (domain_type T) then
+                  do_robust_set_operation T accum
+                else if is_sel s then
+                  if constr_name_for_sel_like s = @{const_name FunBox} then
+                    let val dom_C = ctype_for (domain_type T) in
+                      (CFun (dom_C, S Minus, dom_C), accum)
+                    end
+                  else
+                    (ctype_for_sel cdata x, accum)
+                else if is_constr thy stds x then
+                  (ctype_for_constr cdata x, accum)
+                else if is_built_in_const thy stds fast_descrs x then
+                  case def_of_const thy def_table x of
+                    SOME t' => do_term t' accum
+                  | NONE => (print_g ("*** built-in " ^ s); unsolvable)
+                else
+                  let val C = ctype_for T in
+                    (C, ({bounds = bounds, frees = frees,
+                          consts = (x, C) :: consts}, cset))
+                  end)
          | Free (x as (_, T)) =>
            (case AList.lookup (op =) frees x of
               SOME C => (C, accum)
@@ -881,20 +885,21 @@
 val bounteous_consts = [@{const_name bisim}]
 
 (* term -> bool *)
-fun is_harmless_axiom t =
-  Term.add_consts t [] |> filter_out (is_built_in_const true)
+fun is_harmless_axiom ({thy, stds, fast_descrs, ...} : hol_context) t =
+  Term.add_consts t []
+  |> filter_out (is_built_in_const thy stds fast_descrs)
   |> (forall (member (op =) harmless_consts o original_name o fst)
       orf exists (member (op =) bounteous_consts o fst))
 
 (* cdata -> sign -> term -> accumulator -> accumulator *)
-fun consider_nondefinitional_axiom cdata sn t =
-  not (is_harmless_axiom t) ? consider_general_formula cdata sn t
+fun consider_nondefinitional_axiom (cdata as {hol_ctxt, ...}) sn t =
+  not (is_harmless_axiom hol_ctxt t) ? consider_general_formula cdata sn t
 
 (* cdata -> term -> accumulator -> accumulator *)
 fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
   if not (is_constr_pattern_formula thy t) then
     consider_nondefinitional_axiom cdata Plus t
-  else if is_harmless_axiom t then
+  else if is_harmless_axiom hol_ctxt t then
     I
   else
     let
diff -r 15a5f213ef5b -r 2bcdae5f4fdb src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Thu Feb 18 18:48:07 2010 +0100
@@ -467,7 +467,7 @@
   | factorize z = [z]
 
 (* hol_context -> op2 -> term -> nut *)
-fun nut_from_term (hol_ctxt as {thy, fast_descrs, special_funs, ...}) eq =
+fun nut_from_term (hol_ctxt as {thy, stds, fast_descrs, special_funs, ...}) eq =
   let
     (* string list -> typ list -> term -> nut *)
     fun aux eq ss Ts t =
@@ -603,46 +603,62 @@
              Const (@{const_name top}, _) => Cst (False, bool_T, Any)
            | _ => Op1 (Finite, bool_T, Any, sub t1))
         | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
-        | (Const (@{const_name zero_nat_inst.zero_nat}, T), []) =>
-          Cst (Num 0, T, Any)
-        | (Const (@{const_name one_nat_inst.one_nat}, T), []) =>
-          Cst (Num 1, T, Any)
-        | (Const (@{const_name plus_nat_inst.plus_nat}, T), []) =>
-          Cst (Add, T, Any)
-        | (Const (@{const_name minus_nat_inst.minus_nat}, T), []) =>
-          Cst (Subtract, T, Any)
-        | (Const (@{const_name times_nat_inst.times_nat}, T), []) =>
-          Cst (Multiply, T, Any)
-        | (Const (@{const_name div_nat_inst.div_nat}, T), []) =>
-          Cst (Divide, T, Any)
-        | (Const (@{const_name ord_nat_inst.less_nat}, T), [t1, t2]) =>
-          Op2 (Less, bool_T, Any, sub t1, sub t2)
-        | (Const (@{const_name ord_nat_inst.less_eq_nat}, T), [t1, t2]) =>
-          Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
+        | (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)
+        | (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)
+        | (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
+          if is_built_in_const thy stds false x then Cst (Add, T, Any)
+          else ConstName (s, T, Any)
+        | (Const (@{const_name minus_class.minus},
+                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+           [t1, t2]) =>
+          Op2 (SetDifference, T1, Any, sub t1, sub t2)
+        | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
+          if is_built_in_const thy stds false x then Cst (Subtract, T, Any)
+          else ConstName (s, T, Any)
+        | (Const (x as (s as @{const_name times_class.times}, T)), []) =>
+          if is_built_in_const thy stds false x then Cst (Multiply, T, Any)
+          else ConstName (s, T, Any)
+        | (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)),
+           ts as [t1, t2]) =>
+          if is_built_in_const thy stds false x then
+            Op2 (Less, bool_T, Any, sub t1, sub t2)
+          else
+            do_apply t0 ts
+        | (Const (@{const_name ord_class.less_eq},
+                  Type ("fun", [Type ("fun", [_, @{typ bool}]), _])),
+           [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)),
+           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))
+          else
+            do_apply t0 ts
         | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
         | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
-        | (Const (@{const_name zero_int_inst.zero_int}, T), []) =>
-          Cst (Num 0, T, Any)
-        | (Const (@{const_name one_int_inst.one_int}, T), []) =>
-          Cst (Num 1, T, Any)
-        | (Const (@{const_name plus_int_inst.plus_int}, T), []) =>
-          Cst (Add, T, Any)
-        | (Const (@{const_name minus_int_inst.minus_int}, T), []) =>
-          Cst (Subtract, T, Any)
-        | (Const (@{const_name times_int_inst.times_int}, T), []) =>
-          Cst (Multiply, T, Any)
-        | (Const (@{const_name div_int_inst.div_int}, T), []) =>
-          Cst (Divide, T, Any)
-        | (Const (@{const_name uminus_int_inst.uminus_int}, T), []) =>
-          let val num_T = domain_type T in
-            Op2 (Apply, num_T --> num_T, Any,
-                 Cst (Subtract, num_T --> num_T --> num_T, Any),
-                 Cst (Num 0, num_T, Any))
-          end
-        | (Const (@{const_name ord_int_inst.less_int}, T), [t1, t2]) =>
-          Op2 (Less, bool_T, Any, sub t1, sub t2)
-        | (Const (@{const_name ord_int_inst.less_eq_int}, T), [t1, t2]) =>
-          Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
+        | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
+          if is_built_in_const thy stds false x then
+            let val num_T = domain_type T in
+              Op2 (Apply, num_T --> num_T, Any,
+                   Cst (Subtract, num_T --> num_T --> num_T, Any),
+                   Cst (Num 0, num_T, Any))
+            end
+          else
+            ConstName (s, T, Any)
         | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
         | (Const (@{const_name is_unknown}, T), [t1]) =>
           Op1 (IsUnknown, bool_T, Any, sub t1)
@@ -655,18 +671,16 @@
         | (Const (@{const_name of_nat},
                   T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
           Cst (NatToInt, T, Any)
-        | (Const (@{const_name semilattice_inf_fun_inst.inf_fun}, T),
-                  [t1, t2]) =>
-          Op2 (Intersect, nth_range_type 2 T, Any, sub t1, sub t2)
-        | (Const (@{const_name semilattice_sup_fun_inst.sup_fun}, T),
-                  [t1, t2]) =>
-          Op2 (Union, nth_range_type 2 T, Any, sub t1, sub t2)
-        | (t0 as Const (@{const_name minus_fun_inst.minus_fun}, T), [t1, t2]) =>
-          Op2 (SetDifference, nth_range_type 2 T, Any, sub t1, sub t2)
-        | (t0 as Const (@{const_name ord_fun_inst.less_eq_fun}, T), [t1, t2]) =>
-          Op2 (Subset, bool_T, Any, sub t1, sub t2)
+        | (Const (@{const_name semilattice_inf_class.inf},
+                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+           [t1, t2]) =>
+          Op2 (Intersect, T1, Any, sub t1, sub t2)
+        | (Const (@{const_name semilattice_sup_class.sup},
+                  Type ("fun", [T1 as Type ("fun", [_, @{typ bool}]), _])),
+           [t1, t2]) =>
+          Op2 (Union, T1, Any, sub t1, sub t2)
         | (t0 as Const (x as (s, T)), ts) =>
-          if is_constr thy x then
+          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)
@@ -678,7 +692,7 @@
           else if String.isPrefix numeral_prefix s then
             Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
           else
-            (case arity_of_built_in_const fast_descrs x of
+            (case arity_of_built_in_const thy stds fast_descrs x of
                SOME n =>
                (case n - length ts of
                   0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])
diff -r 15a5f213ef5b -r 2bcdae5f4fdb src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 18 18:48:07 2010 +0100
@@ -43,11 +43,9 @@
   | may_use_binary_ints _ = true
 fun should_use_binary_ints (t1 $ t2) =
     should_use_binary_ints t1 orelse should_use_binary_ints t2
-  | should_use_binary_ints (Const (s, _)) =
-    member (op =) [@{const_name times_nat_inst.times_nat},
-                   @{const_name div_nat_inst.div_nat},
-                   @{const_name times_int_inst.times_int},
-                   @{const_name div_int_inst.div_int}] s orelse
+  | should_use_binary_ints (Const (s, T)) =
+    ((s = @{const_name times} orelse s = @{const_name div}) andalso
+     is_integer_type (body_type T)) orelse
     (String.isPrefix numeral_prefix s andalso
      let val n = the (Int.fromString (unprefix numeral_prefix s)) in
        n < ~ binary_int_threshold orelse n > binary_int_threshold
@@ -65,7 +63,8 @@
         let val table = aux t2 [] table in aux t1 (t2 :: args) table end
       | aux (Abs (_, _, t')) _ table = aux t' [] table
       | aux (t as Const (x as (s, _))) args table =
-        if is_built_in_const true x orelse is_constr_like thy x orelse
+        if is_built_in_const thy [(NONE, true)] true x orelse
+           is_constr_like thy x orelse
            is_sel s orelse s = @{const_name Sigma} then
           table
         else
@@ -119,7 +118,7 @@
 (** Boxing **)
 
 (* hol_context -> typ -> term -> term *)
-fun constr_expand (hol_ctxt as {thy, ...}) T t =
+fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
   (case head_of t of
      Const x => if is_constr_like thy x then t else raise SAME ()
    | _ => raise SAME ())
@@ -134,12 +133,13 @@
                datatype_constrs hol_ctxt T |> hd
            val arg_Ts = binder_types T'
          in
-           list_comb (Const x', map2 (select_nth_constr_arg thy x' t)
+           list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
                                      (index_seq 0 (length arg_Ts)) arg_Ts)
          end
 
 (* hol_context -> bool -> term -> term *)
-fun box_fun_and_pair_in_term (hol_ctxt as {thy, fast_descrs, ...}) def orig_t =
+fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
+                             orig_t =
   let
     (* typ -> typ *)
     fun box_relational_operator_type (Type ("fun", Ts)) =
@@ -172,8 +172,9 @@
                      |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
              |> Envir.eta_contract
              |> new_s <> "fun"
-                ? construct_value thy (@{const_name FunBox},
-                                       Type ("fun", new_Ts) --> new_T) o single
+                ? construct_value thy stds
+                      (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
+                      o single
            | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
                                \coerce_term", [t']))
         | (Type (new_s, new_Ts as [new_T1, new_T2]),
@@ -185,12 +186,12 @@
               if new_s = "fun" then
                 coerce_term Ts new_T (Type ("fun", old_Ts)) t1
               else
-                construct_value thy
+                construct_value thy stds
                     (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
-                     [coerce_term Ts (Type ("fun", new_Ts))
-                                  (Type ("fun", old_Ts)) t1]
+                    [coerce_term Ts (Type ("fun", new_Ts))
+                                 (Type ("fun", old_Ts)) t1]
             | Const _ $ t1 $ t2 =>
-              construct_value thy
+              construct_value thy stds
                   (if new_s = "*" then @{const_name Pair}
                    else @{const_name PairBox}, new_Ts ---> new_T)
                   [coerce_term Ts new_T1 old_T1 t1,
@@ -302,7 +303,7 @@
         Const (s, if s = @{const_name converse} orelse
                      s = @{const_name trancl} then
                     box_relational_operator_type T
-                  else if is_built_in_const fast_descrs x orelse
+                  else if is_built_in_const thy stds fast_descrs x orelse
                           s = @{const_name Sigma} then
                     T
                   else if is_constr_like thy x then
@@ -325,7 +326,7 @@
           betapply (if s1 = "fun" then
                       t1
                     else
-                      select_nth_constr_arg thy
+                      select_nth_constr_arg thy stds
                           (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
                           (Type ("fun", Ts1)), t2)
         end
@@ -341,7 +342,7 @@
           betapply (if s1 = "fun" then
                       t1
                     else
-                      select_nth_constr_arg thy
+                      select_nth_constr_arg thy stds
                           (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
                           (Type ("fun", Ts1)), t2)
         end
@@ -371,13 +372,14 @@
       | aux _ = true
   in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
 
-(* theory -> typ list -> bool -> int -> int -> term -> term list -> term list
-   -> term * term list *)
-fun pull_out_constr_comb thy Ts relax k level t args seen =
+(* hol_context -> typ list -> bool -> int -> int -> term -> term list
+   -> term list -> term * term list *)
+fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t
+                         args seen =
   let val t_comb = list_comb (t, args) in
     case t of
       Const x =>
-      if not relax andalso is_constr thy x andalso
+      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
          not (loose_bvar (t_comb, level)) then
@@ -398,8 +400,8 @@
          (index_seq 0 n) seen
   end
 
-(* theory -> bool -> term -> term *)
-fun pull_out_universal_constrs thy def t =
+(* hol_context -> bool -> term -> term *)
+fun pull_out_universal_constrs hol_ctxt def t =
   let
     val k = maxidx_of_term t + 1
     (* typ list -> bool -> term -> term list -> term list -> term * term list *)
@@ -421,7 +423,7 @@
         let val (t2, seen) = do_term Ts def t2 [] seen in
           do_term Ts def t1 (t2 :: args) seen
         end
-      | _ => pull_out_constr_comb thy Ts def k 0 t args seen
+      | _ => pull_out_constr_comb hol_ctxt Ts def k 0 t args seen
     (* typ list -> bool -> bool -> term -> term -> term -> term list
        -> term * term list *)
     and do_eq_or_imp Ts eq def t0 t1 t2 seen =
@@ -440,8 +442,8 @@
 fun mk_exists v t =
   HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
 
-(* theory -> term -> term *)
-fun pull_out_existential_constrs thy t =
+(* hol_context -> term -> term *)
+fun pull_out_existential_constrs hol_ctxt t =
   let
     val k = maxidx_of_term t + 1
     (* typ list -> int -> term -> term list -> term list -> term * term list *)
@@ -468,13 +470,13 @@
         in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
       | _ =>
         if num_exists > 0 then
-          pull_out_constr_comb thy Ts false k num_exists t args seen
+          pull_out_constr_comb hol_ctxt Ts false k num_exists t args seen
         else
           (list_comb (t, args), seen)
   in aux [] 0 t [] [] |> fst end
 
 (* hol_context -> bool -> term -> term *)
-fun destroy_pulled_out_constrs (hol_ctxt as {thy, ...}) axiom t =
+fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
   let
     (* styp -> int *)
     val num_occs_of_var =
@@ -509,7 +511,7 @@
         | (Const (x as (s, T)), args) =>
           let val arg_Ts = binder_types T in
             if length arg_Ts = length args andalso
-               (is_constr thy x orelse s = @{const_name Pair}) andalso
+               (is_constr thy stds x orelse s = @{const_name Pair}) andalso
                (not careful orelse not (is_Var t1) orelse
                 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
               discriminate_value hol_ctxt x t1 ::
@@ -524,7 +526,8 @@
                         else t0 $ aux false t2 $ aux false t1
     (* styp -> term -> int -> typ -> term -> term *)
     and sel_eq x t n nth_T nth_t =
-      HOLogic.eq_const nth_T $ nth_t $ select_nth_constr_arg thy x t n nth_T
+      HOLogic.eq_const nth_T $ nth_t
+                             $ select_nth_constr_arg thy stds x t n nth_T
       |> aux false
   in aux axiom t end
 
@@ -565,34 +568,40 @@
         aux (t1 :: prems) (Term.add_vars t1 zs) t2
   in aux [] [] end
 
-(* theory -> int -> term list -> term list -> (term * term list) option *)
-fun find_bound_assign _ _ _ [] = NONE
-  | find_bound_assign thy j seen (t :: ts) =
-    let
-      (* bool -> term -> term -> (term * term list) option *)
-      fun aux pass1 t1 t2 =
-        (if loose_bvar1 (t2, j) then
-           if pass1 then aux false t2 t1 else raise SAME ()
-         else case t1 of
-           Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
-         | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
-           if j' = j andalso
-              s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
-             SOME (construct_value thy (@{const_name FunBox}, T2 --> T1) [t2],
-                   ts @ seen)
-           else
-             raise SAME ()
-         | _ => raise SAME ())
-        handle SAME () => find_bound_assign thy j (t :: seen) ts
-    in
-      case t of
-        Const (@{const_name "op ="}, _) $ t1 $ t2 => aux true t1 t2
-      | _ => find_bound_assign thy j (t :: seen) ts
-    end
+(* theory -> (typ option * bool) list -> int -> term list -> term list
+   -> (term * term list) option *)
+fun find_bound_assign thy stds j =
+  let
+    (* term list -> term list -> (term * term list) option *)
+    fun do_term _ [] = NONE
+      | do_term seen (t :: ts) =
+        let
+          (* bool -> term -> term -> (term * term list) option *)
+          fun do_eq pass1 t1 t2 =
+            (if loose_bvar1 (t2, j) then
+               if pass1 then do_eq false t2 t1 else raise SAME ()
+             else case t1 of
+               Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
+             | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
+               if j' = j andalso
+                  s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
+                 SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
+                                       [t2], ts @ seen)
+               else
+                 raise SAME ()
+             | _ => raise SAME ())
+            handle SAME () => do_term (t :: seen) ts
+        in
+          case t of
+            Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2
+          | _ => do_term (t :: seen) ts
+        end
+  in do_term end
 
 (* int -> term -> term -> term *)
 fun subst_one_bound j arg t =
   let
+    (* term * int -> term *)
     fun aux (Bound i, lev) =
         if i < lev then raise SAME ()
         else if i = lev then incr_boundvars (lev - j) arg
@@ -604,13 +613,13 @@
       | aux _ = raise SAME ()
   in aux (t, j) handle SAME () => t end
 
-(* theory -> term -> term *)
-fun destroy_existential_equalities thy =
+(* hol_context -> term -> term *)
+fun destroy_existential_equalities ({thy, stds, ...} : hol_context) =
   let
     (* string list -> typ list -> term list -> term *)
     fun kill [] [] ts = foldr1 s_conj ts
       | kill (s :: ss) (T :: Ts) ts =
-        (case find_bound_assign thy (length ss) [] ts of
+        (case find_bound_assign thy stds (length ss) [] ts of
            SOME (_, []) => @{const True}
          | SOME (arg_t, ts) =>
            kill ss Ts (map (subst_one_bound (length ss)
@@ -704,13 +713,11 @@
               val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
               val (pref, connective, set_oper) =
                 if gfp then
-                  (lbfp_prefix,
-                   @{const "op |"},
-                   @{const_name semilattice_sup_fun_inst.sup_fun})
+                  (lbfp_prefix, @{const "op |"},
+                   @{const_name semilattice_sup_class.sup})
                 else
-                  (ubfp_prefix,
-                   @{const "op &"},
-                   @{const_name semilattice_inf_fun_inst.inf_fun})
+                  (ubfp_prefix, @{const "op &"},
+                   @{const_name semilattice_inf_class.inf})
               (* unit -> term *)
               fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
                            |> aux ss Ts js depth polar
@@ -854,7 +861,7 @@
                                            (index_seq 0 (length args) ~~ args)
                 val _ = not (null eligible_args) orelse raise SAME ()
                 val old_axs = equational_fun_axioms hol_ctxt x
-                              |> map (destroy_existential_equalities thy)
+                              |> map (destroy_existential_equalities hol_ctxt)
                 val static_params = static_args_in_terms hol_ctxt x old_axs
                 val fixed_js = overlapping_indices static_params eligible_args
                 val _ = not (null fixed_js) orelse raise SAME ()
@@ -1016,8 +1023,8 @@
 
 (* hol_context -> term -> (term list * term list) * (bool * bool) *)
 fun axioms_for_term
-        (hol_ctxt as {thy, max_bisim_depth, user_axioms, fast_descrs, evals,
-                      def_table, nondef_table, user_nondefs, ...}) t =
+        (hol_ctxt as {thy, max_bisim_depth, stds, user_axioms, fast_descrs,
+                      evals, def_table, nondef_table, user_nondefs, ...}) t =
   let
     type accumulator = styp list * (term list * term list)
     (* (term list * term list -> term list)
@@ -1051,7 +1058,8 @@
       case t of
         t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
       | Const (x as (s, T)) =>
-        (if member (op =) xs x orelse is_built_in_const fast_descrs x then
+        (if member (op =) xs x orelse
+            is_built_in_const thy stds fast_descrs x then
            accum
          else
            let val accum as (xs, _) = (x :: xs, axs) in
@@ -1072,7 +1080,7 @@
                  fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
                       accum
                end
-             else if is_constr thy x then
+             else if is_constr thy stds x then
                accum
              else if is_equational_fun hol_ctxt x then
                fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
@@ -1127,7 +1135,7 @@
         #> (if is_pure_typedef thy T then
               fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
             else if is_quot_type thy T then
-              fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
+              fold (add_def_axiom depth) (optimized_quot_type_axioms thy stds z)
             else if max_bisim_depth >= 0 andalso is_codatatype thy T then
               fold (add_maybe_def_axiom depth)
                    (codatatype_bisim_axioms hol_ctxt T)
@@ -1377,8 +1385,8 @@
 
 (* hol_context -> term
    -> ((term list * term list) * (bool * bool)) * term * bool *)
-fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
-                                  skolemize, uncurry, ...}) t =
+fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
+                                  boxes, skolemize, uncurry, ...}) t =
   let
     val skolem_depth = if skolemize then 4 else ~1
     val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
@@ -1388,12 +1396,12 @@
                      |> specialize_consts_in_term hol_ctxt 0
                      |> `(axioms_for_term hol_ctxt)
     val binarize =
+      is_standard_datatype thy stds nat_T andalso
       case binary_ints of
         SOME false => false
-      | _ =>
-        forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
-        (binary_ints = SOME true orelse
-         exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
+      | _ => forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
+             (binary_ints = SOME true orelse
+              exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
     val box = exists (not_equal (SOME false) o snd) boxes
     val table =
       Termtab.empty |> uncurry
@@ -1403,12 +1411,12 @@
       binarize ? binarize_nat_and_int_in_term
       #> uncurry ? uncurry_term table
       #> box ? box_fun_and_pair_in_term hol_ctxt def
-      #> destroy_constrs ? (pull_out_universal_constrs thy def
-                            #> pull_out_existential_constrs thy
+      #> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
+                            #> pull_out_existential_constrs hol_ctxt
                             #> destroy_pulled_out_constrs hol_ctxt def)
       #> curry_assms
       #> destroy_universal_equalities
-      #> destroy_existential_equalities thy
+      #> destroy_existential_equalities hol_ctxt
       #> simplify_constrs_and_sels thy
       #> distribute_quantifiers
       #> push_quantifiers_inward thy
diff -r 15a5f213ef5b -r 2bcdae5f4fdb src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Feb 18 18:48:07 2010 +0100
@@ -111,7 +111,7 @@
   | is_complete_type dtypes (Type ("*", Ts)) =
     forall (is_complete_type dtypes) Ts
   | is_complete_type dtypes T =
-    not (is_integer_type T) andalso not (is_bit_type T) andalso
+    not (is_integer_like_type T) andalso not (is_bit_type T) andalso
     #complete (the (datatype_spec dtypes T))
     handle Option.Option => true
 and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
@@ -135,8 +135,9 @@
 
 (* (string -> string) -> scope
    -> string list * string list * string list * string list * string list *)
-fun quintuple_for_scope quote ({hol_ctxt as {thy, ctxt, ...}, card_assigns,
-                                bits, bisim_depth, datatypes, ...} : scope) =
+fun quintuple_for_scope quote
+        ({hol_ctxt as {thy, ctxt, stds, ...}, card_assigns, bits, bisim_depth,
+         datatypes, ...} : scope) =
   let
     val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
                      @{typ bisim_iterator}]
@@ -144,7 +145,7 @@
       card_assigns |> filter_out (member (op =) boring_Ts o fst)
                    |> List.partition (is_fp_iterator_type o fst)
     val (secondary_card_assigns, primary_card_assigns) =
-      card_assigns |> List.partition ((is_integer_type orf is_datatype thy)
+      card_assigns |> List.partition ((is_integer_type orf is_datatype thy stds)
                                       o fst)
     val cards =
       map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
@@ -400,7 +401,8 @@
        -> int Typtab.table *)
     fun aux next _ [] = Typtab.update_new (dummyT, next)
       | aux next reusable ((T, k) :: assigns) =
-        if k = 1 orelse is_integer_type T orelse is_bit_type T then
+        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
           aux next reusable assigns
         else if length (these (Option.map #constrs (datatype_spec dtypes T)))
                 > 1 then
@@ -468,19 +470,20 @@
   end
 
 (* hol_context -> bool -> typ list -> scope_desc -> typ * int -> dtype_spec *)
-fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ...}) binarize
+fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, stds, ...}) binarize
         deep_dataTs (desc as (card_assigns, _)) (T, card) =
   let
     val deep = member (op =) deep_dataTs T
     val co = is_codatatype thy T
-    val standard = is_standard_datatype hol_ctxt T
+    val standard = is_standard_datatype thy stds T
     val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
     val self_recs = map (is_self_recursive_constr_type o snd) xs
     val (num_self_recs, num_non_self_recs) =
       List.partition I self_recs |> pairself length
     val complete = has_exact_card hol_ctxt card_assigns T
-    val concrete = xs |> maps (binder_types o snd) |> maps binder_types
-                      |> forall (has_exact_card hol_ctxt card_assigns)
+    val concrete = is_word_type T orelse
+                   (xs |> maps (binder_types o snd) |> maps binder_types
+                       |> forall (has_exact_card hol_ctxt card_assigns))
     (* int -> int *)
     fun sum_dom_cards max =
       map (domain_card max card_assigns o snd) xs |> Integer.sum
@@ -502,12 +505,12 @@
         (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, ...}) binarize sym_break
+fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break
                           deep_dataTs (desc as (card_assigns, _)) =
   let
     val datatypes =
       map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
-               desc) (filter (is_datatype thy o fst) card_assigns)
+               desc) (filter (is_datatype thy stds o fst) card_assigns)
     val bits = card_of_type card_assigns @{typ signed_bit} - 1
                handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
                       card_of_type card_assigns @{typ unsigned_bit}
diff -r 15a5f213ef5b -r 2bcdae5f4fdb src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Feb 18 10:38:37 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Feb 18 18:48:07 2010 +0100
@@ -215,10 +215,11 @@
     SOME z => SOME z
   | NONE => ps |> find_first (is_none o fst) |> Option.map snd
 (* (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option *)
-fun triple_lookup eq ps key =
-  case AList.lookup (op =) ps (SOME key) of
-    SOME z => SOME z
-  | NONE => double_lookup eq ps key
+fun triple_lookup _ [(NONE, z)] _ = SOME z
+  | triple_lookup eq ps key =
+    case AList.lookup (op =) ps (SOME key) of
+      SOME z => SOME z
+    | NONE => double_lookup eq ps key
 
 (* string -> string -> bool *)
 fun is_substring_of needle stack =