--- a/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Tue Sep 11 13:06:13 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Tue Sep 11 13:06:14 2012 +0200
@@ -12,7 +12,6 @@
val dest_listT: typ -> typ
val mk_Cons: term -> term -> term
- val mk_If: term -> term -> term -> term
val mk_Shift: term -> term -> term
val mk_Succ: term -> term -> term
val mk_Times: term * term -> term
@@ -122,10 +121,6 @@
fun mk_size t = HOLogic.size_const (fastype_of t) $ t;
-fun mk_If p t f =
- let val T = fastype_of t;
- in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end;
-
fun mk_quotient A R =
let val T = fastype_of A;
in Const (@{const_name quotient}, T --> fastype_of R --> HOLogic.mk_setT T) $ A $ R end;