1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 27 15:55:36 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Oct 27 16:52:06 2009 +0100
     1.3 @@ -125,7 +125,7 @@
     1.4    val is_inductive_pred : extended_context -> styp -> bool
     1.5    val is_constr_pattern_lhs : theory -> term -> bool
     1.6    val is_constr_pattern_formula : theory -> term -> bool
     1.7 -  val coalesce_type_vars_in_terms : term list -> term list
     1.8 +  val merge_type_vars_in_terms : term list -> term list
     1.9    val ground_types_in_type : extended_context -> typ -> typ list
    1.10    val ground_types_in_terms : extended_context -> term list -> typ list
    1.11    val format_type : int list -> int list -> typ -> typ
    1.12 @@ -1016,24 +1016,6 @@
    1.13        | do_eq _ = false
    1.14    in do_eq end
    1.15  
    1.16 -(* This table is not pretty. A better approach would be to avoid expanding the
    1.17 -   operators to their low-level definitions, but this would require dealing with
    1.18 -   overloading. *)
    1.19 -val built_in_built_in_defs =
    1.20 -  [@{thm div_int_inst.div_int}, @{thm div_int_inst.mod_int},
    1.21 -   @{thm div_nat_inst.div_nat}, @{thm div_nat_inst.mod_nat},
    1.22 -   @{thm lower_semilattice_fun_inst.inf_fun}, @{thm minus_fun_inst.minus_fun},
    1.23 -   @{thm minus_int_inst.minus_int}, @{thm minus_nat_inst.minus_nat},
    1.24 -   @{thm one_int_inst.one_int}, @{thm one_nat_inst.one_nat},
    1.25 -   @{thm ord_fun_inst.less_eq_fun}, @{thm ord_int_inst.less_eq_int},
    1.26 -   @{thm ord_int_inst.less_int}, @{thm ord_nat_inst.less_eq_nat},
    1.27 -   @{thm ord_nat_inst.less_nat}, @{thm plus_int_inst.plus_int},
    1.28 -   @{thm plus_nat_inst.plus_nat}, @{thm times_int_inst.times_int},
    1.29 -   @{thm times_nat_inst.times_nat}, @{thm uminus_int_inst.uminus_int},
    1.30 -   @{thm upper_semilattice_fun_inst.sup_fun}, @{thm zero_int_inst.zero_int},
    1.31 -   @{thm zero_nat_inst.zero_nat}]
    1.32 -  |> map prop_of
    1.33 -
    1.34  (* theory -> term list * term list * term list *)
    1.35  fun all_axioms_of thy =
    1.36    let
    1.37 @@ -1054,8 +1036,7 @@
    1.38      val (built_in_nondefs, user_nondefs) =
    1.39        List.partition (is_typedef_axiom thy false) user_nondefs
    1.40        |>> append built_in_nondefs
    1.41 -    val defs = built_in_built_in_defs @
    1.42 -               (thy |> PureThy.all_thms_of
    1.43 +    val defs = (thy |> PureThy.all_thms_of
    1.44                      |> filter (equal Thm.definitionK o Thm.get_kind o snd)
    1.45                      |> map (prop_of o snd) |> filter is_plain_definition) @
    1.46                 user_defs @ built_in_defs
    1.47 @@ -1309,10 +1290,6 @@
    1.48      |> fold_rev (curry absdummy) (func_Ts @ [dataT])
    1.49    end
    1.50  
    1.51 -val redefined_in_Nitpick_thy =
    1.52 -  [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},
    1.53 -   @{const_name list_size}]
    1.54 -
    1.55  (* theory -> string -> typ -> typ -> term -> term *)
    1.56  fun optimized_record_get thy s rec_T res_T t =
    1.57    let val constr_x = the_single (datatype_constrs thy rec_T) in
    1.58 @@ -1382,7 +1359,6 @@
    1.59    (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
    1.60     orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
    1.61    andf (not o has_trivial_definition thy def_table)
    1.62 -  andf (not o member (op =) redefined_in_Nitpick_thy o fst)
    1.63  
    1.64  (* term * term -> term *)
    1.65  fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
    1.66 @@ -1879,9 +1855,7 @@
    1.67  (* extended_context -> styp -> term list *)
    1.68  fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
    1.69                                              psimp_table, ...}) (x as (s, _)) =
    1.70 -  if s mem redefined_in_Nitpick_thy then
    1.71 -    []
    1.72 -  else case def_props_for_const thy fast_descrs (!simp_table) x of
    1.73 +  case def_props_for_const thy fast_descrs (!simp_table) x of
    1.74      [] => (case def_props_for_const thy fast_descrs psimp_table x of
    1.75               [] => [inductive_pred_axiom ext_ctxt x]
    1.76             | psimps => psimps)
    1.77 @@ -1890,7 +1864,7 @@
    1.78  val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
    1.79  
    1.80  (* term list -> term list *)
    1.81 -fun coalesce_type_vars_in_terms ts =
    1.82 +fun merge_type_vars_in_terms ts =
    1.83    let
    1.84      (* typ -> (sort * string) list -> (sort * string) list *)
    1.85      fun add_type (TFree (s, S)) table =