add_abbrev: check tfrees of rhs, not tvars (addresses a lapse introduced in 1.65);

--- a/src/Pure/type.ML	Thu Jun 19 15:47:26 2008 +0200
+++ b/src/Pure/type.ML	Thu Jun 19 17:32:18 2008 +0200
@@ -587,7 +587,7 @@
     (case duplicates (op =) vs of
       [] => []
     | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
-    (case subtract (op =) vs (map (#1 o #1) (typ_tvars rhs')) of
+    (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
       [] => []
     | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
     types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))