src/HOL/hologic.ML

   val exists_const: typ -> term
   val choice_const: typ -> term
   val Collect_const: typ -> term
   val mk_eq: term * term -> term
   val dest_eq: term -> term * term
-  val dest_eq_typ: term -> (term * term) * typ
   val mk_all: string * typ * term -> term
   val list_all: (string * typ) list * term -> term
   val mk_exists: string * typ * term -> term
   val mk_Collect: string * typ * term -> term
   val class_eq: string

 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 dest_eq_typ (Const ("op =", T) $ lhs $ rhs) = ((lhs, rhs), domain_type T)
-  | dest_eq_typ t = raise TERM ("dest_eq_typ", [t])
-
 fun all_const T = Const ("All", [T --> boolT] ---> boolT);
 fun mk_all (x, T, P) = all_const T $ absfree (x, T, P);
 fun list_all (xs, t) = fold_rev (fn (x, T) => fn P => all_const T $ Abs (x, T, P)) xs t;
 
 fun exists_const T = Const ("Ex", [T --> boolT] ---> boolT);