--- a/src/Pure/meta_simplifier.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/Pure/meta_simplifier.ML Wed Nov 25 09:13:46 2009 +0100
@@ -1163,9 +1163,9 @@
val (rrs', asm') = rules_of_prem ss prem'
in mut_impc prems concl rrss asms (prem' :: prems')
(rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
- ((uncurry take) (i, prems))
+ (take i prems)
(Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
- ((uncurry drop) (i, prems), concl))))) :: eqns)
+ (drop i prems, concl))))) :: eqns)
ss (length prems') ~1
end