# HG changeset patch
# User berghofe
# Date 1098801189 -7200
# Node ID 49f70168f4c0a913cbc66ea0b0e868f83f0c6890
# Parent  ba3c9fdbace32a4911bee2b8519d01f10d8db977
Added function strip_type (for ctyps).

diff -r ba3c9fdbace3 -r 49f70168f4c0 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Oct 26 16:32:09 2004 +0200
+++ b/src/Pure/drule.ML	Tue Oct 26 16:33:09 2004 +0200
@@ -84,6 +84,7 @@
 sig
   include BASIC_DRULE
   val strip_comb: cterm -> cterm * cterm list
+  val strip_type: ctyp -> ctyp list * ctyp
   val rule_attribute: ('a -> thm -> thm) -> 'a attribute
   val tag_rule: tag -> thm -> thm
   val untag_rule: string -> thm -> thm
@@ -197,6 +198,15 @@
       in stripc (ct1, ct2 :: cts) end handle CTERM _ => p
   in stripc (ct, []) end;
 
+(* cterm version of strip_type: maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T) *)
+fun strip_type cT = (case Thm.typ_of cT of
+    Type ("fun", _) =>
+      let
+        val [cT1, cT2] = Thm.dest_ctyp cT;
+        val (cTs, cT') = strip_type cT2
+      in (cT1 :: cTs, cT') end
+  | _ => ([], cT));
+
 
 (** reading of instantiations **)