# HG changeset patch
# User wenzelm
# Date 1162906197 -3600
# Node ID 38013c3a77a22a80a843c3e24849ef7d5601c103
# Parent  0425fc57510fe9141a879922d6244837e77f57b0
tuned hypsubst setup;

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
diff -r 0425fc57510f -r 38013c3a77a2 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Nov 07 14:14:36 2006 +0100
+++ b/src/HOL/HOL.thy	Tue Nov 07 14:29:57 2006 +0100
@@ -864,7 +864,7 @@
 structure Hypsubst = HypsubstFun(
 struct
   structure Simplifier = Simplifier
-  val dest_eq = HOLogic.dest_eq_typ
+  val dest_eq = HOLogic.dest_eq
   val dest_Trueprop = HOLogic.dest_Trueprop
   val dest_imp = HOLogic.dest_imp
   val eq_reflection = HOL.eq_reflection