src/Pure/term.ML

   val is_Var: term -> bool
   val is_TVar: typ -> bool
   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
   val body_type: typ -> typ
   val strip_type: typ -> typ list * typ

   | dest_Free t = raise TERM("dest_Free", [t]);
 
 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;
 
 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)