src/HOL/Tools/Datatype/datatype.ML
changeset 33037 b22e44496dc2
parent 32922 8e40cd05de7a
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -489,7 +489,7 @@
     1.4      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
     1.5        let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
     1.6        in (case duplicates (op =) tvs of
     1.7 -            [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
     1.8 +            [] => if gen_eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
     1.9                    else error ("Mutually recursive datatypes must have same type parameters")
    1.10            | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
    1.11                " : " ^ commas dups))