--- 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);