# HG changeset patch
# User haftmann
# Date 1266573982 -3600
# Node ID d67857e3a8c092602e68169cf96aa16dc13a420d
# Parent  b987b803616d3a1c3c518b829e0d2e7ffa0e73a4
added dest_comb

diff -r b987b803616d -r d67857e3a8c0 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Feb 19 11:06:21 2010 +0100
+++ b/src/Pure/term.ML	Fri Feb 19 11:06:22 2010 +0100
@@ -45,6 +45,7 @@
   val dest_Const: term -> string * typ
   val dest_Free: term -> string * typ
   val dest_Var: term -> indexname * typ
+  val dest_comb: term -> term * term
   val domain_type: typ -> typ
   val range_type: typ -> typ
   val binder_types: typ -> typ list
@@ -278,6 +279,9 @@
 fun dest_Var (Var x) =  x
   | dest_Var t = raise TERM("dest_Var", [t]);
 
+fun dest_comb (t1 $ t2) = (t1, t2)
+  | dest_comb t = raise TERM("dest_comb", [t]);
+
 
 fun domain_type (Type("fun", [T,_])) = T
 and range_type  (Type("fun", [_,T])) = T;