# HG changeset patch
# User haftmann
# Date 1292912601 -3600
# Node ID 481c89fabcbcbd6926d3b3363488494b7e0ed03c
# Parent  ffd730fcf0ac04c141c9e2ac7db6cecf8d514eda
HOLogic.mk_id

diff -r ffd730fcf0ac -r 481c89fabcbc src/HOL/Tools/hologic.ML
--- 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;