src/HOL/BNF/Tools/bnf_fp_util.ML

--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Jan 03 10:48:48 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Fri Jan 03 11:26:44 2014 +0100
@@ -138,6 +138,8 @@
   val mk_sumTN: typ list -> typ
   val mk_sumTN_balanced: typ list -> typ
 
+  val mk_proj: typ -> int -> int -> term
+
   val mk_convol: term * term -> term
 
   val Inl_const: typ -> typ -> term
@@ -374,6 +376,11 @@
 val mk_sumTN = Library.foldr1 mk_sumT;
 val mk_sumTN_balanced = Balanced_Tree.make mk_sumT;
 
+fun mk_proj T n k =
+  let val (binders, _) = strip_typeN n T in
+    fold_rev (fn T => fn t => Abs (Name.uu, T, t)) binders (Bound (n - k - 1))
+  end;
+
 fun mk_convol (f, g) =
   let
     val (fU, fTU) = `range_type (fastype_of f);