src/Pure/conv.ML
changeset 59586 ddf6deaadfe8
parent 56245 84fc7dfa3cd4
child 67721 5348bea4accd
     1.1 --- a/src/Pure/conv.ML	Wed Mar 04 20:50:20 2015 +0100
     1.2 +++ b/src/Pure/conv.ML	Wed Mar 04 22:05:01 2015 +0100
     1.3 @@ -158,7 +158,7 @@
     1.4  
     1.5  fun rewr_conv rule ct =
     1.6    let
     1.7 -    val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
     1.8 +    val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
     1.9      val lhs = Thm.lhs_of rule1;
    1.10      val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
    1.11      val rule3 =