src/HOL/Codatatype/Tools/bnf_fp_util.ML

   val mk_predT: typ -> typ;
 
   val mk_sumTN: typ list -> typ
   val mk_sumTN_balanced: typ list -> typ
 
+  val id_const: typ -> term
+  val id_abs: typ -> term
+
   val Inl_const: typ -> typ -> term
   val Inr_const: typ -> typ -> term
 
   val mk_Inl: typ -> term -> term
   val mk_Inr: typ -> term -> term

   | dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T';
 
 val mk_sumTN = Library.foldr1 mk_sumT;
 val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
 
+fun id_const T = Const (@{const_name id}, T --> T);
+fun id_abs T = Abs (Name.uu, T, Bound 0);
+
 fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
 fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
 
 fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT));
 fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t;