--- a/src/FOL/fologic.ML Mon Jun 23 15:31:25 2008 +0200
+++ b/src/FOL/fologic.ML Mon Jun 23 15:51:37 2008 +0200
@@ -20,7 +20,6 @@
val mk_imp : term * term -> term
val dest_imp : term -> term*term
val dest_conj : term -> term list
- val dest_concls : term -> term list
val mk_iff : term * term -> term
val dest_iff : term -> term*term
val all_const : typ -> term
@@ -67,9 +66,6 @@
fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
| dest_conj t = [t];
-fun imp_concl_of t = imp_concl_of (#2 (dest_imp t)) handle TERM _ => t;
-val dest_concls = map imp_concl_of o dest_conj o dest_Trueprop;
-
fun dest_iff (Const("op <->",_) $ A $ B) = (A, B)
| dest_iff t = raise TERM ("dest_iff", [t]);