src/Pure/more_thm.ML

 val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a);
 val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a);
 val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
 
 
-(* ctyp destructors *)
+(* ctyp operations *)
 
 fun dest_ctyp_fun cT =
-  let
-    val T = Thm.typ_of cT;
-    fun dest_ctyp_nth i = Thm.dest_ctyp_nth i cT;
-  in
-    (case T of
-      Type ("fun", _) => (dest_ctyp_nth 0, dest_ctyp_nth 1)
-    | _ => raise TYPE ("dest_ctyp_fun", [T], []))
-  end;
+  (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], []));
 
 (* 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", _) =>

         val (cTs, cT') = strip_type cT2
       in (cT1 :: cTs, cT') end
   | _ => ([], cT));
 
 
-(* cterm constructors and destructors *)
+(* cterm operations *)
 
 fun all_name ctxt (x, t) A =
   let
     val T = Thm.typ_of_cterm t;
     val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T --> propT) --> propT));