# 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 **)