--- 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 *)