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