diff -r 38013c3a77a2 -r e1063a0e6dfd src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Tue Nov 07 14:29:57 2006 +0100
+++ b/src/HOL/hologic.ML	Tue Nov 07 14:29:58 2006 +0100
@@ -38,7 +38,6 @@
   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
@@ -156,9 +155,6 @@
 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;