src/HOL/Codatatype/Tools/bnf_fp_util.ML

   val dest_sumTN: int -> typ -> typ list
   val dest_sumTN_balanced: int -> typ -> typ list
   val dest_tupleT: int -> typ -> typ list
 
   val mk_Field: term -> term
+  val mk_If: term -> term -> term -> term
   val mk_union: term * term -> term
 
   val mk_sumEN: int -> thm
   val mk_sumEN_balanced: int -> thm
   val mk_sum_casesN: int -> int -> thm

   end;
 
 val mk_sum_caseN = Library.foldr1 mk_sum_case;
 val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case;
 
+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_Field r =
   let val T = fst (dest_relT (fastype_of r));
   in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;
 
 val mk_union = HOLogic.mk_binop @{const_name sup};