New function strip_comb (cterm version of Term.strip_comb).
authorberghofe
Wed Feb 20 16:00:32 2002 +0100 (2002-02-20)
changeset 1290853bfe07a7916
parent 12907 27e6d344d724
child 12909 d3ad295a087a
New function strip_comb (cterm version of Term.strip_comb).
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Wed Feb 20 15:58:38 2002 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Feb 20 16:00:32 2002 +0100
     1.3 @@ -84,6 +84,7 @@
     1.4  signature DRULE =
     1.5  sig
     1.6    include BASIC_DRULE
     1.7 +  val strip_comb: cterm -> cterm * cterm list
     1.8    val rule_attribute: ('a -> thm -> thm) -> 'a attribute
     1.9    val tag_rule: tag -> thm -> thm
    1.10    val untag_rule: string -> thm -> thm
    1.11 @@ -187,6 +188,14 @@
    1.12  fun list_implies([], B) = B
    1.13    | list_implies(A::AS, B) = mk_implies (A, list_implies(AS,B));
    1.14  
    1.15 +(*cterm version of strip_comb: maps  f(t1,...,tn)  to  (f, [t1,...,tn]) *)
    1.16 +fun strip_comb ct = 
    1.17 +  let
    1.18 +    fun stripc (p as (ct, cts)) =
    1.19 +      let val (ct1, ct2) = Thm.dest_comb ct
    1.20 +      in stripc (ct1, ct2 :: cts) end handle CTERM _ => p
    1.21 +  in stripc (ct, []) end;
    1.22 +
    1.23  
    1.24  (** reading of instantiations **)
    1.25