src/HOL/Tools/transfer.ML

   let
     (* identify morphism function *)
     val ([a, D], ctxt2) = ctxt1
       |> Variable.import true (map Drule.mk_term [raw_a, raw_D])
       |>> map Drule.dest_term o snd;
-    val transform = Thm.capply @{cterm "Trueprop"} o Thm.capply D;
+    val transform = Thm.apply @{cterm "Trueprop"} o Thm.apply D;
     val T = Thm.typ_of (Thm.ctyp_of_term a);
     val (aT, bT) = (Term.range_type T, Term.domain_type T);
     
     (* determine variables to transfer *)
     val ctxt3 = ctxt2

     val vars = filter (fn ((v, _), T) => Type.could_unify (T, aT) andalso
       not (member (op =) leave v)) (Term.add_vars (Thm.prop_of thm) []);
     val c_vars = map (certify o Var) vars;
     val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3;
     val c_vars' = map (certify o (fn v => Free (v, bT))) vs';
-    val c_exprs' = map (Thm.capply a) c_vars';
+    val c_exprs' = map (Thm.apply a) c_vars';
 
     (* transfer *)
     val (hyps, ctxt5) = ctxt4
       |> Assumption.add_assumes (map transform c_vars');
     val simpset =