# HG changeset patch
# User wenzelm
# Date 1158858331 -7200
# Node ID 27738ccd0700ce30541e15c003d51652ff31720d
# Parent  b96394d8c702b5307638db059587ba7cb2498868
added dest_binop;

diff -r b96394d8c702 -r 27738ccd0700 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Sep 21 19:05:22 2006 +0200
+++ b/src/Pure/thm.ML	Thu Sep 21 19:05:31 2006 +0200
@@ -135,6 +135,7 @@
   val dest_ctyp: ctyp -> ctyp list
   val dest_comb: cterm -> cterm * cterm
   val dest_arg: cterm -> cterm
+  val dest_binop: cterm -> cterm * cterm
   val dest_abs: string option -> cterm -> cterm * cterm
   val adjust_maxidx_cterm: int -> cterm -> cterm
   val capply: cterm -> cterm -> cterm
@@ -272,6 +273,15 @@
       end
   | dest_arg _ = raise CTERM "dest_arg";
 
+fun dest_binop (Cterm {t = tm, T = _, thy_ref, maxidx, sorts}) =
+  let fun cterm t T = Cterm {t = t, T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} in
+    (case tm of
+      Const (_, Type ("fun", [A, Type ("fun", [B, _])])) $ a $ b => (cterm a A, cterm b B)
+    |  Free (_, Type ("fun", [A, Type ("fun", [B, _])])) $ a $ b => (cterm a A, cterm b B)
+    |   Var (_, Type ("fun", [A, Type ("fun", [B, _])])) $ a $ b => (cterm a A, cterm b B)
+    | _ => raise CTERM "dest_binop")
+  end;
+
 fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
       let val (y', t') = Term.dest_abs (the_default x a, T, t) in
         (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},