New function strip_comb (cterm version of Term.strip_comb).

--- a/src/Pure/drule.ML	Wed Feb 20 15:58:38 2002 +0100
+++ b/src/Pure/drule.ML	Wed Feb 20 16:00:32 2002 +0100
@@ -84,6 +84,7 @@
 signature DRULE =
 sig
   include BASIC_DRULE
+  val strip_comb: cterm -> cterm * cterm list
   val rule_attribute: ('a -> thm -> thm) -> 'a attribute
   val tag_rule: tag -> thm -> thm
   val untag_rule: string -> thm -> thm
@@ -187,6 +188,14 @@
 fun list_implies([], B) = B
   | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B));
 
+(*cterm version of strip_comb: maps  f(t1,...,tn)  to  (f, [t1,...,tn]) *)
+fun strip_comb ct = 
+  let
+    fun stripc (p as (ct, cts)) =
+      let val (ct1, ct2) = Thm.dest_comb ct
+      in stripc (ct1, ct2 :: cts) end handle CTERM _ => p
+  in stripc (ct, []) end;
+
 
 (** reading of instantiations **)