--- a/src/HOL/BNF/Tools/bnf_lfp_util.ML Tue Dec 17 15:44:10 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_util.ML Tue Dec 17 15:56:57 2013 +0100
@@ -12,7 +12,6 @@
val mk_bij_betw: term -> term -> term -> term
val mk_cardSuc: term -> term
- val mk_cpow: term -> term
val mk_inver: term -> term -> term -> term
val mk_not_empty: term -> term
val mk_not_eq: term -> term -> term
@@ -49,10 +48,6 @@
let val T = fst (dest_relT (fastype_of r));
in Const (@{const_name cardSuc}, mk_relT (T, T) --> mk_relT (`I (HOLogic.mk_setT T))) $ r end;
-fun mk_cpow r =
- let val T = fst (dest_relT (fastype_of r));
- in Const (@{const_name cpow}, mk_relT (T, T) --> mk_relT (`I (HOLogic.mk_setT T))) $ r end;
-
fun mk_bij_betw f A B =
Const (@{const_name bij_betw},
fastype_of f --> fastype_of A --> fastype_of B --> HOLogic.boolT) $ f $ A $ B;