diff -r 7ba65fe66c73 -r 305390f23734 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Tue Dec 23 11:37:48 1997 +0100
+++ b/src/FOL/ROOT.ML	Tue Dec 23 11:39:03 1997 +0100
@@ -28,9 +28,10 @@
 structure Hypsubst_Data =
   struct
   structure Simplifier = Simplifier
-    (*Take apart an equality judgement; otherwise raise Match!*)
-  fun dest_eq (Const("Trueprop",_) $ (Const("op =",T)  $ t $ u)) = 
-	(t, u, domain_type T)
+    (*These destructors  Match!*)
+  fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
+  val dest_Trueprop = FOLogic.dest_Trueprop
+  val dest_imp = FOLogic.dest_imp
   val eq_reflection = eq_reflection
   val imp_intr = impI
   val rev_mp = rev_mp