# HG changeset patch
# User wenzelm
# Date 1214229097 -7200
# Node ID 70e4eb732fa97dbfaf4b707639c347183e469f8f
# Parent  904acdaf42996da47258a03b1cfba655702e4480
removed obsolete dest_concls;

diff -r 904acdaf4299 -r 70e4eb732fa9 src/FOL/fologic.ML
--- 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]);
 
diff -r 904acdaf4299 -r 70e4eb732fa9 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Mon Jun 23 15:31:25 2008 +0200
+++ b/src/HOL/hologic.ML	Mon Jun 23 15:51:37 2008 +0200
@@ -34,7 +34,6 @@
   val disjuncts: term -> term list
   val dest_imp: term -> term * term
   val dest_not: term -> term
-  val dest_concls: term -> term list
   val eq_const: typ -> term
   val mk_eq: term * term -> term
   val dest_eq: term -> term * term
@@ -198,9 +197,6 @@
 fun dest_not (Const ("Not", _) $ t) = t
   | dest_not t = raise TERM ("dest_not", [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 eq_const T = Const ("op =", [T, T] ---> boolT);
 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;