more precise "incremented" indication, which might be relevant in corner cases, e.g. instantiation of leading to vars with different types (which is a potential problem nonetheless);

--- a/src/Pure/drule.ML	Wed May 29 18:25:11 2013 +0200
+++ b/src/Pure/drule.ML	Wed May 29 18:52:35 2013 +0200
@@ -368,12 +368,6 @@
     [th] => th
   | _ => raise THM ("compose: unique result expected", i, [tha,thb]));
 
-(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
-fun tha COMP thb =
-  (case compose(tha, 1, thb) of
-    [th] => th
-  | _ => raise THM ("COMP", 1, [tha, thb]));
-
 
 (** theorem equality **)
 
@@ -740,8 +734,21 @@
 fun incr_indexes2 th1 th2 =
   Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1);
 
-fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2;
-fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2;
+local
+
+(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*)
+fun comp incremented th1 th2 =
+  Thm.bicompose {flatten = true, match = false, incremented = incremented} (false, th1, 0) 1 th2
+  |> Seq.list_of |> distinct Thm.eq_thm
+  |> (fn [th] => th | _ => raise THM ("COMP", 1, [th1, th2]));
+
+in
+
+fun th1 COMP th2 = comp false th1 th2;
+fun th1 INCR_COMP th2 = comp true (incr_indexes th2 th1) th2;
+fun th1 COMP_INCR th2 = comp true th1 (incr_indexes th1 th2);
+
+end;
 
 fun comp_no_flatten (th, n) i rule =
   (case distinct Thm.eq_thm (Seq.list_of