src/HOL/Tools/Nitpick/nitpick_hol.ML

   val ersatz_table : theory -> (string * string) list
   val def_of_const : theory -> const_table -> styp -> term option
   val is_inductive_pred : extended_context -> styp -> bool
   val is_constr_pattern_lhs : theory -> term -> bool
   val is_constr_pattern_formula : theory -> term -> bool
-  val coalesce_type_vars_in_terms : term list -> term list
+  val merge_type_vars_in_terms : term list -> term list
   val ground_types_in_type : extended_context -> typ -> typ list
   val ground_types_in_terms : extended_context -> term list -> typ list
   val format_type : int list -> int list -> typ -> typ
   val format_term_type :
     theory -> const_table -> (term option * int list) list -> term -> typ

       | do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
         do_lhs t1
       | do_eq _ = false
   in do_eq end
 
-(* This table is not pretty. A better approach would be to avoid expanding the
-   operators to their low-level definitions, but this would require dealing with
-   overloading. *)
-val built_in_built_in_defs =
-  [@{thm div_int_inst.div_int}, @{thm div_int_inst.mod_int},
-   @{thm div_nat_inst.div_nat}, @{thm div_nat_inst.mod_nat},
-   @{thm lower_semilattice_fun_inst.inf_fun}, @{thm minus_fun_inst.minus_fun},
-   @{thm minus_int_inst.minus_int}, @{thm minus_nat_inst.minus_nat},
-   @{thm one_int_inst.one_int}, @{thm one_nat_inst.one_nat},
-   @{thm ord_fun_inst.less_eq_fun}, @{thm ord_int_inst.less_eq_int},
-   @{thm ord_int_inst.less_int}, @{thm ord_nat_inst.less_eq_nat},
-   @{thm ord_nat_inst.less_nat}, @{thm plus_int_inst.plus_int},
-   @{thm plus_nat_inst.plus_nat}, @{thm times_int_inst.times_int},
-   @{thm times_nat_inst.times_nat}, @{thm uminus_int_inst.uminus_int},
-   @{thm upper_semilattice_fun_inst.sup_fun}, @{thm zero_int_inst.zero_int},
-   @{thm zero_nat_inst.zero_nat}]
-  |> map prop_of
-
 (* theory -> term list * term list * term list *)
 fun all_axioms_of thy =
   let
     (* theory list -> term list *)
     val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)

     val (user_defs, user_nondefs) =
       partition_axioms_by_definitionality thy user_axioms def_names
     val (built_in_nondefs, user_nondefs) =
       List.partition (is_typedef_axiom thy false) user_nondefs
       |>> append built_in_nondefs
-    val defs = built_in_built_in_defs @
-               (thy |> PureThy.all_thms_of
+    val defs = (thy |> PureThy.all_thms_of
                     |> filter (equal Thm.definitionK o Thm.get_kind o snd)
                     |> map (prop_of o snd) |> filter is_plain_definition) @
                user_defs @ built_in_defs
   in (defs, built_in_nondefs, user_nondefs) end
 

     constr_case_body thy (1, x)
     |> fold_rev (add_constr_case thy res_T) (length xs downto 2 ~~ xs')
     |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   end
 
-val redefined_in_Nitpick_thy =
-  [@{const_name option_case}, @{const_name nat_case}, @{const_name list_case},
-   @{const_name list_size}]
-
 (* theory -> string -> typ -> typ -> term -> term *)
 fun optimized_record_get thy s rec_T res_T t =
   let val constr_x = the_single (datatype_constrs thy rec_T) in
     case no_of_record_field thy s rec_T of
       ~1 => (case rec_T of

   is_real_inductive_pred ext_ctxt andf (not o is_real_equational_fun ext_ctxt)
 fun is_equational_fun (ext_ctxt as {thy, def_table, ...}) =
   (is_real_equational_fun ext_ctxt orf is_real_inductive_pred ext_ctxt
    orf (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst)
   andf (not o has_trivial_definition thy def_table)
-  andf (not o member (op =) redefined_in_Nitpick_thy o fst)
 
 (* term * term -> term *)
 fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t
   | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t
   | s_betapply p = betapply p

     raw_inductive_pred_axiom ext_ctxt x
 
 (* extended_context -> styp -> term list *)
 fun raw_equational_fun_axioms (ext_ctxt as {thy, fast_descrs, simp_table,
                                             psimp_table, ...}) (x as (s, _)) =
-  if s mem redefined_in_Nitpick_thy then
-    []
-  else case def_props_for_const thy fast_descrs (!simp_table) x of
+  case def_props_for_const thy fast_descrs (!simp_table) x of
     [] => (case def_props_for_const thy fast_descrs psimp_table x of
              [] => [inductive_pred_axiom ext_ctxt x]
            | psimps => psimps)
   | simps => simps
 
 val equational_fun_axioms = map extensionalize oo raw_equational_fun_axioms
 
 (* term list -> term list *)
-fun coalesce_type_vars_in_terms ts =
+fun merge_type_vars_in_terms ts =
   let
     (* typ -> (sort * string) list -> (sort * string) list *)
     fun add_type (TFree (s, S)) table =
         (case AList.lookup (op =) table S of
            SOME s' =>