src/Pure/type.ML
changeset 20951 868120282837
parent 20674 93baed0f741c
child 21116 be58cded79da
     1.1 --- a/src/Pure/type.ML	Tue Oct 10 13:59:12 2006 +0200
     1.2 +++ b/src/Pure/type.ML	Tue Oct 10 13:59:13 2006 +0200
     1.3 @@ -552,7 +552,7 @@
     1.4      (case duplicates (op =) vs of
     1.5        [] => []
     1.6      | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
     1.7 -    (case gen_rems (op =) (map (#1 o #1) (typ_tvars rhs'), vs) of
     1.8 +    (case subtract (op =) vs (map (#1 o #1) (typ_tvars rhs')) of
     1.9        [] => []
    1.10      | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
    1.11      types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))