diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Pure/thm.ML	Wed May 29 18:25:11 2013 +0200
@@ -144,8 +144,8 @@
   val permute_prems: int -> int -> thm -> thm
   val rename_params_rule: string list * int -> thm -> thm
   val rename_boundvars: term -> term -> thm -> thm
-  val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
-  val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
+  val bicompose: {flatten: bool, match: bool, incremented: bool} ->
+    bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   val extern_oracles: Proof.context -> (Markup.T * xstring) list
   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
@@ -1615,7 +1615,7 @@
 *)
 local exception COMPOSE
 in
-fun bicompose_aux flatten match (state, (stpairs, Bs, Bi, C), lifted)
+fun bicompose_aux {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted)
                         (eres_flg, orule, nsubgoal) =
  let val Thm (sder, {maxidx=smax, shyps=sshyps, hyps=shyps, ...}) = state
      and Thm (rder, {maxidx=rmax, shyps=rshyps, hyps=rhyps,
@@ -1705,17 +1705,14 @@
 
      val env0 = Envir.empty (Int.max (rmax, smax));
  in
-   (case if lifted then SOME env0 else unify_var_types thy (state, orule) env0 of
+   (case if incremented then SOME env0 else unify_var_types thy (state, orule) env0 of
      NONE => Seq.empty
    | SOME env => if eres_flg then eres env (rev rAs) else res env)
  end;
 end;
 
-fun compose_no_flatten match (orule, nsubgoal) i state =
-  bicompose_aux false match (state, dest_state (state, i), false) (false, orule, nsubgoal);
-
-fun bicompose match arg i state =
-  bicompose_aux true match (state, dest_state (state,i), false) arg;
+fun bicompose flags arg i state =
+  bicompose_aux flags (state, dest_state (state,i), false) arg;
 
 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
@@ -1733,7 +1730,9 @@
         val lift = lift_rule (cprem_of state i);
         val B = Logic.strip_assums_concl Bi;
         val Hs = Logic.strip_assums_hyp Bi;
-        val compose = bicompose_aux true match (state, (stpairs, Bs, Bi, C), true);
+        val compose =
+          bicompose_aux {flatten = true, match = match, incremented = true}
+            (state, (stpairs, Bs, Bi, C), true);
         fun res [] = Seq.empty
           | res ((eres_flg, rule)::brules) =
               if !Pattern.trace_unify_fail orelse