# HG changeset patch
# User paulson
# Date 916740999 -3600
# Node ID af32e2c3f77ae50dd3044889672876b45160d3ef
# Parent  26abad27b03c921bf39f91817952163140f75b4b
tidied; added dest_eq

diff -r 26abad27b03c -r af32e2c3f77a src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Tue Jan 19 11:16:07 1999 +0100
+++ b/src/FOL/fologic.ML	Tue Jan 19 11:16:39 1999 +0100
@@ -7,19 +7,20 @@
 
 signature FOLOGIC =
 sig
-  val oT: typ
-  val mk_Trueprop: term -> term
-  val dest_Trueprop: term -> term
-  val dest_imp	       : term -> term*term
-  val conj: term
-  val disj: term
-  val imp: term
-  val eq_const: typ -> term
-  val all_const: typ -> term
-  val exists_const: typ -> term
-  val mk_eq: term * term -> term
-  val mk_all: term * term -> term
-  val mk_exists: term * term -> term
+  val oT		: typ
+  val mk_Trueprop	: term -> term
+  val dest_Trueprop	: term -> term
+  val conj		: term
+  val disj		: term
+  val imp		: term
+  val dest_imp	       	: term -> term*term
+  val all_const		: typ -> term
+  val mk_all		: term * term -> term
+  val exists_const	: typ -> term
+  val mk_exists		: term * term -> term
+  val eq_const		: typ -> term
+  val mk_eq		: term * term -> term
+  val dest_eq 		: term -> term*term
 end;
 
 
@@ -47,6 +48,9 @@
 fun eq_const T = Const ("op =", [T, T] ---> oT);
 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 --> oT] ---> oT);
 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));