Added function strip_type (for ctyps).

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