diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Pure/tactic.ML	Wed May 29 18:25:11 2013 +0200
@@ -111,7 +111,8 @@
 
 (*The composition rule/state: no lifting or var renaming.
   The arg = (bires_flg, orule, m);  see Thm.bicompose for explanation.*)
-fun compose_tac arg i = PRIMSEQ (Thm.bicompose false arg i);
+fun compose_tac arg i =
+  PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = false} arg i);
 
 (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
   like [| P&Q; P==>R |] ==> R *)