src/Pure/thm.ML

   val dest_fun: cterm -> cterm
   val dest_arg: cterm -> cterm
   val dest_fun2: cterm -> cterm
   val dest_arg1: cterm -> cterm
   val dest_abs: string option -> cterm -> cterm * cterm
-  val capply: cterm -> cterm -> cterm
-  val cabs_name: string * cterm -> cterm -> cterm
-  val cabs: cterm -> cterm -> cterm
+  val apply: cterm -> cterm -> cterm
+  val lambda_name: string * cterm -> cterm -> cterm
+  val lambda: cterm -> cterm -> cterm
   val adjust_maxidx_cterm: int -> cterm -> cterm
   val incr_indexes_cterm: int -> cterm -> cterm
   val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   val fold_terms: (term -> 'a -> 'a) -> thm -> 'a -> 'a

   | dest_abs _ ct = raise CTERM ("dest_abs", [ct]);
 
 
 (* constructors *)
 
-fun capply
+fun apply
   (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...})
   (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) =
     if T = dty then
       Cterm {thy_ref = merge_thys0 cf cx,
         t = f $ x,
         T = rty,
         maxidx = Int.max (maxidx1, maxidx2),
         sorts = Sorts.union sorts1 sorts2}
-      else raise CTERM ("capply: types don't agree", [cf, cx])
-  | capply cf cx = raise CTERM ("capply: first arg is not a function", [cf, cx]);
-
-fun cabs_name
+      else raise CTERM ("apply: types don't agree", [cf, cx])
+  | apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]);
+
+fun lambda_name
   (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
   (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) =
     let val t = Term.lambda_name (x, t1) t2 in
       Cterm {thy_ref = merge_thys0 ct1 ct2,
         t = t, T = T1 --> T2,
         maxidx = Int.max (maxidx1, maxidx2),
         sorts = Sorts.union sorts1 sorts2}
     end;
 
-fun cabs t u = cabs_name ("", t) u;
+fun lambda t u = lambda_name ("", t) u;
 
 
 (* indexes *)
 
 fun adjust_maxidx_cterm i (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =

               if clash then del_clashing false xs xs qs [] else qs
           | del_clashing clash xs ys ((p as (x, y)) :: ps) qs =
               if member (op =) ys y
               then del_clashing true (x :: xs) (x :: ys) ps qs
               else del_clashing clash xs (y :: ys) ps (p :: qs);
-        val al'' = del_clashing false unchanged unchanged al' [];        
+        val al'' = del_clashing false unchanged unchanged al' [];
         fun rename (t as Var ((x, i), T)) =
               (case AList.lookup (op =) al'' x of
                  SOME y => Var ((y, i), T)
                | NONE => t)
           | rename (Abs (x, T, t)) =