src/Pure/thm.ML

 (*Calls error rather than raising an exception because it is intended
   for top-level use -- exception handling would not make sense here.
   The names in cs, if distinct, are used for the innermost parameters;
    preceding parameters may be renamed to make all params distinct.*)
 fun rename_params_rule (cs, i) state =
-  let val Thm{sign,der,maxidx,hyps,prop,...} = state
+  let val Thm{sign,der,maxidx,hyps,...} = state
       val (tpairs, Bs, Bi, C) = dest_state(state,i)
       val iparams = map #1 (Logic.strip_params Bi)
       val short = length iparams - length cs
       val newnames =
             if short<0 then error"More names than abstractions!"
             else variantlist(take (short,iparams), cs) @ cs
-      val freenames = map (#1 o dest_Free) (term_frees prop)
+      val freenames = map (#1 o dest_Free) (term_frees Bi)
       val newBi = Logic.list_rename_params (newnames, Bi)
   in
   case findrep cs of
      c::_ => error ("Bound variables not distinct: " ^ c)
    | [] => (case cs inter_string freenames of