diff -r 2673979cb54d -r 8ff45c2076da src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Apr 29 01:11:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Apr 29 01:17:14 2010 +0200
@@ -57,6 +57,8 @@
   val bool_T : typ
   val nat_T : typ
   val int_T : typ
+  val monomorphic_term : Type.tyenv -> term -> term
+  val specialize_type : theory -> (string * typ) -> term -> term
   val nat_subscript : int -> string
   val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
   val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
@@ -227,6 +229,9 @@
 val nat_T = @{typ nat}
 val int_T = @{typ int}
 
+val monomorphic_term = Sledgehammer_Util.monomorphic_term
+val specialize_type = Sledgehammer_Util.specialize_type
+
 val subscript = implode o map (prefix "\<^isub>") o explode
 fun nat_subscript n =
   (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit