--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 11 13:06:13 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 11 13:06:14 2012 +0200
@@ -101,6 +101,7 @@
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
@@ -258,6 +259,10 @@
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;