1.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Feb 06 11:00:24 2006 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Feb 06 11:01:28 2006 +0100
     1.3 @@ -200,7 +200,7 @@
     1.4        else ["Illegal schematic variable(s) on rhs"];
     1.5  
     1.6      val dup_lhs_tfrees =
     1.7 -      (case duplicates lhs_tfrees of [] => []
     1.8 +      (case gen_duplicates (op =) lhs_tfrees of [] => []
     1.9        | dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
    1.10  
    1.11      val extra_rhs_tfrees =