src/HOL/Tools/Nitpick/nitpick_util.ML

   val instantiate_type : theory -> typ -> typ -> typ -> typ
   val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
   val varify_and_instantiate_type_global : theory -> typ -> typ -> typ -> typ
   val is_of_class_const : theory -> string * typ -> bool
   val get_class_def : theory -> string -> (string * term) option
-  val monomorphic_term : Type.tyenv -> term -> term
   val specialize_type : theory -> string * typ -> term -> term
   val eta_expand : typ list -> term -> int -> term
   val DETERM_TIMEOUT : Time.time -> tactic -> tactic
   val indent_size : int
   val pretty_maybe_quote : Keyword.keywords -> Pretty.T -> Pretty.T

   let val axname = class ^ "_class_def" in
     Option.map (pair axname)
       (AList.lookup (op =) (Theory.all_axioms_of thy) axname)
   end;
 
-val monomorphic_term = ATP_Util.monomorphic_term
 val specialize_type = ATP_Util.specialize_type
 val eta_expand = ATP_Util.eta_expand
 
 fun DETERM_TIMEOUT delay tac st =
   Seq.of_list (the_list (TimeLimit.timeLimit delay (fn () => SINGLE tac st) ()))