Now rename_params_rule merely issues warnings--and does nothing--if the
authorpaulson
Wed Jul 23 11:54:32 1997 +0200 (1997-07-23)
changeset 3565c64410e701fb
parent 3564 f886dbd91ee5
child 3566 c9c351374651
Now rename_params_rule merely issues warnings--and does nothing--if the
renaming cannot be performed. Previously it raised a fatal error.
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Wed Jul 23 11:52:22 1997 +0200
     1.2 +++ b/src/Pure/thm.ML	Wed Jul 23 11:54:32 1997 +0200
     1.3 @@ -1217,9 +1217,11 @@
     1.4        val newBi = Logic.list_rename_params (newnames, Bi)
     1.5    in
     1.6    case findrep cs of
     1.7 -     c::_ => error ("Bound variables not distinct: " ^ c)
     1.8 +     c::_ => (warning ("Can't rename.  Bound variables not distinct: " ^ c); 
     1.9 +	      state)
    1.10     | [] => (case cs inter_string freenames of
    1.11 -       a::_ => error ("Bound/Free variable clash: " ^ a)
    1.12 +       a::_ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); 
    1.13 +		state)
    1.14       | [] => fix_shyps [state] []
    1.15                  (Thm{sign = sign,
    1.16                       der = infer_derivs (Rename_params_rule(cs,i), [der]),