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