COMP now performs a distinctness check on the multiple results before failing

--- a/src/Pure/drule.ML	Tue Feb 13 10:09:21 2007 +0100
+++ b/src/Pure/drule.ML	Tue Feb 13 16:37:14 2007 +0100
@@ -557,7 +557,7 @@
 
 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
 fun tha COMP thb =
-    case compose(tha,1,thb) of
+    case distinct eq_thm (compose(tha,1,thb)) of
         [th] => th
       | _ =>   raise THM("COMP", 1, [tha,thb]);