# HG changeset patch
# User paulson
# Date 869651672 -7200
# Node ID c64410e701fbd3af985b5ac813fbf17da30ac9c0
# Parent  f886dbd91ee58e17253b797e10dfb9c633752c4c
Now rename_params_rule merely issues warnings--and does nothing--if the
renaming cannot be performed.  Previously it raised a fatal error.

diff -r f886dbd91ee5 -r c64410e701fb src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Jul 23 11:52:22 1997 +0200
+++ b/src/Pure/thm.ML	Wed Jul 23 11:54:32 1997 +0200
@@ -1217,9 +1217,11 @@
       val newBi = Logic.list_rename_params (newnames, Bi)
   in
   case findrep cs of
-     c::_ => error ("Bound variables not distinct: " ^ c)
+     c::_ => (warning ("Can't rename.  Bound variables not distinct: " ^ c); 
+	      state)
    | [] => (case cs inter_string freenames of
-       a::_ => error ("Bound/Free variable clash: " ^ a)
+       a::_ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); 
+		state)
      | [] => fix_shyps [state] []
                 (Thm{sign = sign,
                      der = infer_derivs (Rename_params_rule(cs,i), [der]),