diff -r 52e636ace94e -r 323414474c1f src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 16 06:51:36 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 16 10:33:25 2012 +0200
@@ -92,7 +92,6 @@
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
-  val strip_typeN: int -> typ -> typ list * typ
   val retype_free: typ -> term -> term
 
   val mk_predT: typ -> typ;
@@ -241,9 +240,6 @@
 
 val mk_common_name = space_implode "_" o map Binding.name_of;
 
-fun strip_typeN 0 T = ([], T)
-  | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T;
-
 fun mk_predT T = T --> HOLogic.boolT;
 
 fun retype_free T (Free (s, _)) = Free (s, T);