diff -r 0425fc57510f -r 38013c3a77a2 src/FOL/hypsubstdata.ML
--- a/src/FOL/hypsubstdata.ML	Tue Nov 07 14:14:36 2006 +0100
+++ b/src/FOL/hypsubstdata.ML	Tue Nov 07 14:29:57 2006 +0100
@@ -3,7 +3,7 @@
 structure Hypsubst_Data =
 struct
   structure Simplifier = Simplifier
-  fun dest_eq (Const("op =",T) $ t $ u) = ((t, u), domain_type T)
+  val dest_eq = FOLogic.dest_eq
   val dest_Trueprop = FOLogic.dest_Trueprop
   val dest_imp = FOLogic.dest_imp
   val eq_reflection = eq_reflection