src/Pure/meta_simplifier.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 16042 8e15ff79851a
--- a/src/Pure/meta_simplifier.ML	Fri Mar 04 11:44:26 2005 +0100
+++ b/src/Pure/meta_simplifier.ML	Fri Mar 04 15:07:34 2005 +0100
@@ -1059,9 +1059,9 @@
                 find_index_eq p tprems) (#hyps (rep_thm eqn)));
               val (rrs', asm') = rules_of_prem ss prem'
             in mut_impc prems concl rrss asms (prem' :: prems')
-              (rrs' :: rrss') (asm' :: asms') (SOME (Library.foldr (disch true)
-                (Library.take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies
-                  (Library.drop (i, prems), concl))))) :: eqns) ss (length prems') ~1
+              (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true)
+                (Drule.imp_cong' eqn (reflexive (Drule.list_implies
+                  (Library.drop (i, prems), concl)))) (Library.take (i, prems))) :: eqns) ss (length prems') ~1
             end
 
      (*legacy code - only for backwards compatibility*)