# HG changeset patch
# User berghofe
# Date 1014217232 -3600
# Node ID 53bfe07a79164d80e8f1b244e40821d2ad4ca0cb
# Parent  27e6d344d724e93513306b28d26da2e717abdf16
New function strip_comb (cterm version of Term.strip_comb).

diff -r 27e6d344d724 -r 53bfe07a7916 src/Pure/drule.ML
--- 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 **)