# HG changeset patch
# User wenzelm
# Date 921674783 -3600
# Node ID 32fda1090a13b127e23ac5f7bc0718006f5088b0
# Parent  2b17ff28a6ccebdc0a45d9f16d4acc63d362e2ac
added dest_mem;

diff -r 2b17ff28a6cc -r 32fda1090a13 src/HOL/hologic.ML
--- 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 *)