diff -r 5018f6a76b3f -r cffdb7b28498 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML	Wed Oct 21 10:15:31 2009 +0200
@@ -370,7 +370,8 @@
 fun iter_type_class_pairs thy tycons [] = ([], [])
   | iter_type_class_pairs thy tycons classes =
       let val cpairs = type_class_pairs thy tycons classes
-          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
+          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
+            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
           val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
       in (union (op =) (classes', classes), union (op =) (cpairs', cpairs)) end;