diff -r 0fa3b456a267 -r 5bb6ae8acb87 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Wed May 29 18:25:11 2013 +0200
@@ -287,7 +287,10 @@
       Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
         (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   in
-    (case Seq.list_of (Thm.bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
+    (case Seq.list_of
+      (Thm.bicompose {flatten = true, match = false, incremented = false}
+        (false, rl, Thm.nprems_of rl) 1 revcut_rl')
+     of
       [th] => th
     | _ => raise THM ("make_elim_preserve", 1, [rl]))
   end;