type_invention_warning : bool ref
# let tm = `x IN s`;; Warning: inventing type variables val tm : term = `x IN s`
# map dest_var (frees tm);; val it : (string * hol_type) list = [("x", `:?47676`); ("s", `:?47676->bool`)]
# let tm = `(x:A) IN s`;; val tm : term = `x IN s`
# type_invention_warning := false;; val it : unit = ()
# SET_RULE `x IN UNIONS (a INSERT t) <=> x IN UNIONS t \/ x IN a`;;