minor optimization
authorblanchet
Wed, 08 Jun 2011 08:47:43 +0200
changeset 441073baf384e2b99
parent 44106 096237fe70f1
child 44108 dd38b8ef52b9
minor optimization
src/HOL/Tools/ATP/atp_translate.ML
     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