diff -r 195b7515911a -r dccd0763ae37 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu May 10 00:39:52 2007 +0200
+++ b/src/Pure/more_thm.ML	Thu May 10 00:39:53 2007 +0200
@@ -2,12 +2,20 @@
     ID:         $Id$
     Author:     Makarius
 
-Further operations on type thm, outside the inference kernel.
+Further operations on type ctyp/cterm/thm, outside the inference kernel.
 *)
 
 signature THM =
 sig
   include THM
+  val mk_binop: cterm -> cterm -> cterm -> cterm
+  val dest_binop: cterm -> cterm * cterm
+  val dest_implies: cterm -> cterm * cterm
+  val dest_equals: cterm -> cterm * cterm
+  val dest_equals_lhs: cterm -> cterm
+  val dest_equals_rhs: cterm -> cterm
+  val lhs_of: thm -> cterm
+  val rhs_of: thm -> cterm
   val thm_ord: thm * thm -> order
   val eq_thm: thm * thm -> bool
   val eq_thms: thm list * thm list -> bool
@@ -41,7 +49,36 @@
 
 (** basic operations **)
 
-(* order: ignores theory context! *)
+(* cterm constructors and destructors *)
+
+fun mk_binop c a b = Thm.capply (Thm.capply c a) b;
+fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct);
+
+fun dest_implies ct =
+  (case Thm.term_of ct of
+    Const ("==>", _) $ _ $ _ => dest_binop ct
+  | _ => raise TERM ("dest_implies", [Thm.term_of ct]));
+
+fun dest_equals ct =
+  (case Thm.term_of ct of
+    Const ("==", _) $ _ $ _ => dest_binop ct
+  | _ => raise TERM ("dest_equals", [Thm.term_of ct]));
+
+fun dest_equals_lhs ct =
+  (case Thm.term_of ct of
+    Const ("==", _) $ _ $ _ => Thm.dest_arg1 ct
+  | _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct]));
+
+fun dest_equals_rhs ct =
+  (case Thm.term_of ct of
+    Const ("==", _) $ _ $ _ => Thm.dest_arg ct
+  | _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct]));
+
+val lhs_of = dest_equals_lhs o Thm.cprop_of;
+val rhs_of = dest_equals_rhs o Thm.cprop_of;
+
+
+(* thm order: ignores theory context! *)
 
 fun thm_ord (th1, th2) =
   let