# HG changeset patch
# User blanchet
# Date 1307515663 -7200
# Node ID 3baf384e2b996d2a2b40882f5fe5f8c3ca7ff4dc
# Parent  096237fe70f18573958ca4652100ed1aa3e1499b
minor optimization

diff -r 096237fe70f1 -r 3baf384e2b99 src/HOL/Tools/ATP/atp_translate.ML
--- 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