Meta all introduction in Isabelle

I'm confused about the all introduction meta rule in Isabelle. The papers say it should be:

From P deduce ⋀ x. P whenever x is not a free variables in the asumptions.

This is confusing to me. I understand better wikipedia's one:

From (P y) deduce ⋀ x. P x whenever y is not free in the (implicit) assumptions and x is not free in P.

How is the meta-forall rule encoded in Isabelle? Here is the source code:

(*Forall introduction.  The Free or Var x must not be free in the hypotheses.
    [x]
     :
     A
  ------
  ⋀x. A
*)
fun forall_intr
    (ct as Cterm {maxidx = maxidx1, t = x, T, sorts, ...})
    (th as Thm (der, {maxidx = maxidx2, shyps, hyps, tpairs, prop, ...})) =
  let
    fun result a =
      Thm (deriv_rule1 (Proofterm.forall_intr_proof x a) der,
       {cert = join_certificate1 (ct, th),
        tags = [],
        maxidx = Int.max (maxidx1, maxidx2),
        shyps = Sorts.union sorts shyps,
        hyps = hyps,
        tpairs = tpairs,
        prop = Logic.all_const T $ Abs (a, T, abstract_over (x, prop))});
    fun check_occs a x ts =
      if exists (fn t => Logic.occs (x, t)) ts then
        raise THM ("forall_intr: variable " ^ quote a ^ " free in assumptions", 0, [th])
      else ();
  in
    (case x of
      Free (a, _) => (check_occs a x hyps; check_occs a x (terms_of_tpairs tpairs); result a)
    | Var ((a, _), _) => (check_occs a x (terms_of_tpairs tpairs); result a)
    | _ => raise THM ("forall_intr: not a variable", 0, [th]))
  end;

Suppose I am a mathematician with only some notions of programming. How would you convince me the piece of code below implements the meta-forall rule in a sensible manner?.