src/Pure/drule.ML

   include BASIC_DRULE
   val outer_params: term -> (string * typ) list
   val generalize: string list * string list -> thm -> thm
   val list_comb: cterm * cterm list -> cterm
   val strip_comb: cterm -> cterm * cterm list
-  val strip_type: ctyp -> ctyp list * ctyp
   val beta_conv: cterm -> cterm -> cterm
   val flexflex_unique: Proof.context option -> thm -> thm
   val export_without_context: thm -> thm
   val export_without_context_open: thm -> thm
   val store_thm: binding -> thm -> thm

     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;
 
-(* 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));
-
 (*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs
   of the meta-equality returned by the beta_conversion rule.*)
 fun beta_conv x y =
   Thm.dest_arg (Thm.cprop_of (Thm.beta_conversion false (Thm.apply x y)));