# HG changeset patch
# User nipkow
# Date 861897595 -7200
# Node ID 99ed078e6ae7e0e99a4cd68e72ae45a2712fc63b
# Parent  5aa3bb94b7290815b8374c3f895953c204d1eb91
rename_params_rule used to check if the new name clashed with a free name in
the whole goal state. Now checks only the subgoal concerned.

diff -r 5aa3bb94b729 -r 99ed078e6ae7 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Apr 24 17:51:27 1997 +0200
+++ b/src/Pure/thm.ML	Thu Apr 24 17:59:55 1997 +0200
@@ -1201,14 +1201,14 @@
   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