# HG changeset patch
# User paulson
# Date 913975215 -3600
# Node ID d9fa148383e2e3a8edf36221a37aacadc17b6672
# Parent  f29d4e5075647969c11c0aee13ad2409bc4de76a
new function dest_eq

diff -r f29d4e507564 -r d9fa148383e2 src/HOL/hologic.ML
--- 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);