--- a/src/HOL/Tools/res_clause.ML Wed Jul 01 16:19:44 2009 +0100
+++ b/src/HOL/Tools/res_clause.ML Thu Jul 02 10:49:46 2009 +0100
@@ -381,8 +381,6 @@
| 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 _ = if null newclasses then ()
- else Output.debug (fn _ => "New classes: " ^ space_implode ", " newclasses)
val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
in (classes' union classes, cpairs' union cpairs) end;