src/Pure/more_thm.ML

   val eq_ctyp: ctyp * ctyp -> bool
   val aconvc: cterm * cterm -> bool
   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
   val mk_binop: cterm -> cterm -> cterm -> cterm
   val dest_binop: cterm -> cterm * cterm

 val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
 
 
 (* 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));