# HG changeset patch
# User blanchet
# Date 1377512081 -7200
# Node ID 2333fae25719de67d9c1956d6b18538b53cc926d
# Parent  2a2dc18f3e10808fddc5e45bb2d4eb79cbf0ae8a
export one more ML function, needed for primcorec

diff -r 2a2dc18f3e10 -r 2333fae25719 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Mon Aug 26 12:14:40 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Mon Aug 26 12:14:41 2013 +0200
@@ -157,6 +157,8 @@
   val dest_sumTN_balanced: int -> typ -> typ list
   val dest_tupleT: int -> typ -> typ list
 
+  val If_const: typ -> term
+
   val mk_Field: term -> term
   val mk_If: term -> term -> term -> term
   val mk_union: term * term -> term
@@ -417,9 +419,8 @@
 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 If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
+fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end;
 
 fun mk_Field r =
   let val T = fst (dest_relT (fastype_of r));