--- a/src/HOL/Tools/Datatype/datatype_aux.ML Tue Oct 20 13:37:56 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Tue Oct 20 16:13:01 2009 +0200
@@ -257,7 +257,7 @@
fun get_nonrec_types descr sorts =
map (typ_of_dtyp descr sorts) (Library.foldl (fn (Ts, (_, (_, _, constrs))) =>
Library.foldl (fn (Ts', (_, cargs)) =>
- filter_out is_rec_type cargs union Ts') (Ts, constrs)) ([], descr));
+ gen_union (op =) (filter_out is_rec_type cargs, Ts')) (Ts, constrs)) ([], descr));
(* get all recursive types in datatype description *)