--- a/src/HOL/hologic.ML Wed Mar 17 13:44:43 1999 +0100
+++ b/src/HOL/hologic.ML Wed Mar 17 13:46:23 1999 +0100
@@ -29,6 +29,7 @@
val mk_exists: string * typ * term -> term
val mk_Collect: string * typ * term -> term
val mk_mem: term * term -> term
+ val dest_mem: term -> term * term
val mk_binop: string -> term * term -> term
val mk_binrel: string -> term * term -> term
val dest_bin: string -> typ -> term -> term * term
@@ -110,6 +111,9 @@
Const ("op :", [dest_setT setT, setT] ---> boolT) $ x $ A
end;
+fun dest_mem (Const ("op :", _) $ x $ A) = (x, A)
+ | dest_mem t = raise TERM ("dest_mem", [t]);
+
(* binary oprations and relations *)