src/Pure/type.ML

       handle TYPE (msg, _, _) => err msg;
   in
     (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'))
   end);