1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 08:47:43 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 08 08:47:43 2011 +0200
1.3 @@ -450,7 +450,7 @@
1.4 val newclasses =
1.5 [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
1.6 val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
1.7 - in (union (op =) classes' classes, union (op =) cpairs' cpairs) end
1.8 + in (classes' @ classes, union (op =) cpairs' cpairs) end
1.9
1.10 fun make_arity_clauses thy tycons =
1.11 iter_type_class_pairs thy tycons ##> multi_arity_clause