--- a/src/Pure/more_thm.ML Sat Apr 13 21:51:24 2019 +0200
+++ b/src/Pure/more_thm.ML Sat Apr 13 22:06:40 2019 +0200
@@ -28,7 +28,7 @@
val add_tvars: thm -> ctyp list -> ctyp list
val add_frees: thm -> cterm list -> cterm list
val add_vars: thm -> cterm list -> cterm list
- val dest_ctyp_fun: ctyp -> ctyp * ctyp
+ val dest_funT: ctyp -> ctyp * ctyp
val strip_type: ctyp -> ctyp list * ctyp
val all_name: Proof.context -> string * cterm -> cterm -> cterm
val all: Proof.context -> cterm -> cterm -> cterm
@@ -146,17 +146,17 @@
(* ctyp operations *)
-fun dest_ctyp_fun cT =
+fun dest_funT cT =
(case Thm.typ_of cT of
Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end
- | T => raise TYPE ("dest_ctyp_fun", [T], []));
+ | T => raise TYPE ("dest_funT", [T], []));
(* ctyp 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) = dest_ctyp_fun cT;
+ val (cT1, cT2) = dest_funT cT;
val (cTs, cT') = strip_type cT2
in (cT1 :: cTs, cT') end
| _ => ([], cT));