--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Dec 01 22:21:40 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Dec 01 22:24:37 2015 +0100
@@ -65,7 +65,6 @@
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
@@ -270,7 +269,6 @@
(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