src/Pure/drule.ML

 (*Generalization over a list of variables*)
 val forall_intr_list = fold_rev Thm.forall_intr;
 
 (*Generalization over Vars -- canonical order*)
 fun forall_intr_vars th =
-  let
-    val vs =
-      build (th |> Thm.fold_atomic_cterms {hyps = false} (fn a =>
-        is_Var (Thm.term_of a) ? insert (op aconvc) a));
+  let val vs = build (th |> Thm.fold_atomic_cterms {hyps = false} Term.is_Var (insert (op aconvc)))
   in fold Thm.forall_intr vs th end;
 
 fun outer_params t =
   let val vs = Term.strip_all_vars t
   in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;