src/Pure/raw_simplifier.ML
changeset 44058 ae85c5d64913
parent 43597 b4a093e755db
child 45290 f599ac41e7f5
     1.1 --- a/src/Pure/raw_simplifier.ML	Mon Aug 08 16:38:59 2011 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Mon Aug 08 17:23:15 2011 +0200
     1.3 @@ -1197,7 +1197,7 @@
     1.4                val prem' = Thm.rhs_of eqn;
     1.5                val tprems = map term_of prems;
     1.6                val i = 1 + fold Integer.max (map (fn p =>
     1.7 -                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
     1.8 +                find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
     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 (fold_rev (disch true)