src/HOL/Tools/Datatype/datatype.ML
changeset 33038 8f9594c31de4
parent 33037 b22e44496dc2
child 33040 cffdb7b28498
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Oct 20 16:13:01 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Oct 21 08:14:38 2009 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4        |> (pairself o map) (fn (_, (tyco, dTs, _)) => (tyco, map (typ_of_dtyp descr vs) dTs));
     1.5      
     1.6      val tycos = map fst dataTs;
     1.7 -    val _ = if gen_eq_set (op =) (tycos, raw_tycos) then ()
     1.8 +    val _ = if eq_set (op =) (tycos, raw_tycos) then ()
     1.9        else error ("Type constructors " ^ commas (map quote raw_tycos)
    1.10          ^ " do not belong exhaustively to one mutual recursive datatype");
    1.11  
    1.12 @@ -489,7 +489,7 @@
    1.13      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
    1.14        let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
    1.15        in (case duplicates (op =) tvs of
    1.16 -            [] => if gen_eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
    1.17 +            [] => if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
    1.18                    else error ("Mutually recursive datatypes must have same type parameters")
    1.19            | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
    1.20                " : " ^ commas dups))