Added function strip_type (for ctyps).
authorberghofe
Tue Oct 26 16:33:09 2004 +0200 (2004-10-26)
changeset 1526249f70168f4c0
parent 15261 ba3c9fdbace3
child 15263 b40e91201039
Added function strip_type (for ctyps).
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Tue Oct 26 16:32:09 2004 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Oct 26 16:33:09 2004 +0200
     1.3 @@ -84,6 +84,7 @@
     1.4  sig
     1.5    include BASIC_DRULE
     1.6    val strip_comb: cterm -> cterm * cterm list
     1.7 +  val strip_type: ctyp -> ctyp list * ctyp
     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 @@ -197,6 +198,15 @@
    1.12        in stripc (ct1, ct2 :: cts) end handle CTERM _ => p
    1.13    in stripc (ct, []) end;
    1.14  
    1.15 +(* cterm version of strip_type: maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T) *)
    1.16 +fun strip_type cT = (case Thm.typ_of cT of
    1.17 +    Type ("fun", _) =>
    1.18 +      let
    1.19 +        val [cT1, cT2] = Thm.dest_ctyp cT;
    1.20 +        val (cTs, cT') = strip_type cT2
    1.21 +      in (cT1 :: cTs, cT') end
    1.22 +  | _ => ([], cT));
    1.23 +
    1.24  
    1.25  (** reading of instantiations **)
    1.26