--- 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)