diff -r fda143b5c2f5 -r ae85c5d64913 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Mon Aug 08 16:38:59 2011 +0200
+++ b/src/Pure/raw_simplifier.ML	Mon Aug 08 17:23:15 2011 +0200
@@ -1197,7 +1197,7 @@
               val prem' = Thm.rhs_of eqn;
               val tprems = map term_of prems;
               val i = 1 + fold Integer.max (map (fn p =>
-                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
+                find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
               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)