--- a/src/HOL/Tools/hologic.ML Wed Dec 01 15:03:44 2010 +0100
+++ b/src/HOL/Tools/hologic.ML Wed Dec 01 15:35:40 2010 +0100
@@ -8,6 +8,7 @@
sig
val typeS: sort
val typeT: typ
+ val mk_comp: term * term -> term
val boolN: string
val boolT: typ
val Trueprop: term
@@ -142,6 +143,16 @@
val typeT = Type_Infer.anyT typeS;
+(* functions *)
+
+fun mk_comp (f, g) =
+ let
+ val fT = fastype_of f;
+ val gT = fastype_of g;
+ val compT = fT --> gT --> domain_type gT --> range_type fT;
+ in Const ("Fun.comp", compT) $ f $ g end;
+
+
(* bool and set *)
val boolN = "HOL.bool";