# HG changeset patch
# User wenzelm
# Date 1003337463 -7200
# Node ID 9eab353e810b975466cf64cd72c4647cc00a6e4a
# Parent  875ee0c20da26754737867ae85efa8f5f11038cd
added mk_UNIV;

diff -r 875ee0c20da2 -r 9eab353e810b src/HOL/hologic.ML
--- 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 *)