src/Pure/thm.ML
changeset 3037 99ed078e6ae7
parent 3012 0d683397b74b
child 3061 25b2a895f864
     1.1 --- a/src/Pure/thm.ML	Thu Apr 24 17:51:27 1997 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Apr 24 17:59:55 1997 +0200
     1.3 @@ -1201,14 +1201,14 @@
     1.4    The names in cs, if distinct, are used for the innermost parameters;
     1.5     preceding parameters may be renamed to make all params distinct.*)
     1.6  fun rename_params_rule (cs, i) state =
     1.7 -  let val Thm{sign,der,maxidx,hyps,prop,...} = state
     1.8 +  let val Thm{sign,der,maxidx,hyps,...} = state
     1.9        val (tpairs, Bs, Bi, C) = dest_state(state,i)
    1.10        val iparams = map #1 (Logic.strip_params Bi)
    1.11        val short = length iparams - length cs
    1.12        val newnames =
    1.13              if short<0 then error"More names than abstractions!"
    1.14              else variantlist(take (short,iparams), cs) @ cs
    1.15 -      val freenames = map (#1 o dest_Free) (term_frees prop)
    1.16 +      val freenames = map (#1 o dest_Free) (term_frees Bi)
    1.17        val newBi = Logic.list_rename_params (newnames, Bi)
    1.18    in
    1.19    case findrep cs of