diff -r 7ba65fe66c73 -r 305390f23734 src/FOL/fologic.ML
--- a/src/FOL/fologic.ML	Tue Dec 23 11:37:48 1997 +0100
+++ b/src/FOL/fologic.ML	Tue Dec 23 11:39:03 1997 +0100
@@ -10,6 +10,7 @@
   val oT: typ
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
+  val dest_imp	       : term -> term*term
   val conj: term
   val disj: term
   val imp: term
@@ -40,6 +41,9 @@
 and disj = Const("op |", [oT,oT]--->oT)
 and imp = Const("op -->", [oT,oT]--->oT);
 
+fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
+  | dest_imp  t = raise TERM ("dest_imp", [t]);
+
 fun eq_const T = Const ("op =", [T, T] ---> oT);
 fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;