HOLogic.mk_id

--- a/src/HOL/Tools/hologic.ML	Tue Dec 21 06:53:20 2010 +0100
+++ b/src/HOL/Tools/hologic.ML	Tue Dec 21 07:23:21 2010 +0100
@@ -8,6 +8,7 @@
 sig
   val typeS: sort
   val typeT: typ
+  val mk_id: typ -> term
   val mk_comp: term * term -> term
   val boolN: string
   val boolT: typ
@@ -145,6 +146,8 @@
 
 (* functions *)
 
+fun mk_id T = Const ("Fun.id", T --> T);
+
 fun mk_comp (f, g) =
   let
     val fT = fastype_of f;