src/Pure/meta_simplifier.ML
changeset 19618 9050a3b01e62
parent 19502 369cde91963d
child 19798 94f12468bbba
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu May 11 19:19:31 2006 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu May 11 19:19:33 2006 +0200
     1.3 @@ -1100,7 +1100,7 @@
     1.4                val prem' = rhs_of eqn;
     1.5                val tprems = map term_of prems;
     1.6                val i = 1 + Library.foldl Int.max (~1, map (fn p =>
     1.7 -                find_index_eq p tprems) (#hyps (rep_thm eqn)));
     1.8 +                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn)));
     1.9                val (rrs', asm') = rules_of_prem ss prem'
    1.10              in mut_impc prems concl rrss asms (prem' :: prems')
    1.11                (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true)