src/Pure/meta_simplifier.ML

           | SOME eqn =>
             let
               val prem' = rhs_of eqn;
               val tprems = map term_of prems;
               val i = 1 + Library.foldl Int.max (~1, map (fn p =>
-                find_index_eq p tprems) (#hyps (rep_thm eqn)));
+                find_index (fn q => q aconv 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 (foldr (disch true)
                 (Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
                   (Library.drop (i, prems), concl)))) (Library.take (i, prems))) :: eqns) ss (length prems') ~1