src/HOL/Tools/Datatype/datatype_aux.ML
changeset 33037 b22e44496dc2
parent 32964 2d7e1ab55037
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -257,7 +257,7 @@
     1.4  fun get_nonrec_types descr sorts =
     1.5    map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
     1.6      Library.foldl (fn (Ts', (_, cargs)) =>
     1.7 -      filter_out is_rec_type cargs union Ts') (Ts, constrs)) ([], descr));
     1.8 +      gen_union (op =) (filter_out is_rec_type cargs, Ts')) (Ts, constrs)) ([], descr));
     1.9  
    1.10  (* get all recursive types in datatype description *)
    1.11