GEN_ALL : thm -> thm
A |- t ------------------ GEN_ALL A |- !x1...xn. t
# let th = ARITH_RULE `x < y ==> 2 * x + y + 1 < 3 * y`;; val th : thm = |- x < y ==> 2 * x + y + 1 < 3 * y # GEN_ALL th;; val it : thm = |- !x y. x < y ==> 2 * x + y + 1 < 3 * y