src/Pure/variable.ML

     val ((xs, ps), ctxt') = focus_params t ctxt;
     val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t);
   in (((xs ~~ ps), t'), ctxt') end;
 
 fun forall_elim_prop t prop =
-  Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t)
+  Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t)
   |> Thm.cprop_of |> Thm.dest_arg;
 
 fun focus_cterm goal ctxt =
   let
     val cert = Thm.cterm_of (Thm.theory_of_cterm goal);