--- 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