src/HOL/Tools/Nunchaku/nunchaku_util.ML

   val plural_s_for_list: 'a list -> string
   val with_overlord_file: string -> string -> (Path.T -> 'a) -> 'a
   val with_tmp_or_overlord_file: bool -> string -> string -> (Path.T -> 'a) -> 'a
   val num_binder_types: typ -> int
   val strip_fun_type: typ -> typ list * typ
-  val attach_typeS: term -> term
   val specialize_type: theory -> string * typ -> term -> term
   val typ_match: theory -> typ * typ -> bool
   val term_match: theory -> term * term -> bool
   val const_match: theory -> (string * typ) * (string * typ) -> bool
   val DETERM_TIMEOUT: Time.time -> tactic -> tactic

   if overlord then with_overlord_file else Isabelle_System.with_tmp_file;
 
 val num_binder_types = BNF_Util.num_binder_types
 val strip_fun_type = BNF_Util.strip_fun_type;
 
-(* Clone from "HOL/Tools/inductive_realizer.ML". *)
-val attach_typeS =
-  map_types (map_atyps
-    (fn TFree (s, []) => TFree (s, \<^sort>\<open>type\<close>)
-      | TVar (ixn, []) => TVar (ixn, \<^sort>\<open>type\<close>)
-      | T => T));
-
 val specialize_type = ATP_Util.specialize_type;
 
 fun typ_match thy TU = can (Sign.typ_match thy TU) Vartab.empty;
 fun term_match thy tu = can (Pattern.match thy tu) (Vartab.empty, Vartab.empty);
 fun const_match thy = term_match thy o apply2 Const;