src/Pure/thm.ML

             else variantlist(take (short,iparams), cs) @ cs
       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)
+     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]),
                      maxidx = maxidx,
                      shyps = [],