--- a/src/HOL/hologic.ML Wed Oct 17 18:50:49 2001 +0200
+++ b/src/HOL/hologic.ML Wed Oct 17 18:51:03 2001 +0200
@@ -40,6 +40,7 @@
val mk_Collect: string * typ * term -> term
val mk_mem: term * term -> term
val dest_mem: term -> term * term
+ val mk_UNIV: typ -> term
val mk_binop: string -> term * term -> term
val mk_binrel: string -> term * term -> term
val dest_bin: string -> typ -> term -> term * term
@@ -152,6 +153,8 @@
fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
| dest_mem t = raise TERM ("dest_mem", [t]);
+fun mk_UNIV T = Const ("UNIV", mk_setT T);
+
(* binary oprations and relations *)