# HG changeset patch
# User wenzelm
# Date 1213889538 -7200
# Node ID d54ae0bdad809c41d2740a94cf20e82fdf5711a7
# Parent  75b251e9cdb7e54752a0beca4af4924f5e76185b
add_abbrev: check tfrees of rhs, not tvars (addresses a lapse introduced in 1.65);

diff -r 75b251e9cdb7 -r d54ae0bdad80 src/Pure/type.ML
--- 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'))