--- a/src/Pure/drule.ML Sat Apr 13 16:33:33 2019 +0200
+++ b/src/Pure/drule.ML Sat Apr 13 16:42:19 2019 +0200
@@ -56,7 +56,6 @@
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
@@ -155,15 +154,6 @@
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 =