--- a/src/HOL/hologic.ML Thu Dec 17 17:45:51 1998 +0100
+++ b/src/HOL/hologic.ML Fri Dec 18 11:00:15 1998 +0100
@@ -24,6 +24,7 @@
val exists_const: typ -> term
val Collect_const: typ -> term
val mk_eq: term * term -> term
+ val dest_eq: term -> term * term
val mk_all: string * typ * term -> term
val mk_exists: string * typ * term -> term
val mk_Collect: string * typ * term -> term
@@ -92,6 +93,9 @@
fun eq_const T = Const ("op =", [T, T] ---> boolT);
fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
+fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
+ | dest_eq t = raise TERM ("dest_eq", [t])
+
fun all_const T = Const ("All", [T --> boolT] ---> boolT);
fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);