src/HOL/hologic.ML

   val dest_conj: term -> term list
   val dest_disj: term -> term list
   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
   val all_const: typ -> term
   val mk_all: string * typ * term -> term

   | dest_imp  t = raise TERM ("dest_imp", [t]);
 
 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;
 
 fun dest_eq (Const ("op =", _) $ lhs $ rhs) = (lhs, rhs)
   | dest_eq t = raise TERM ("dest_eq", [t])