--- 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;