Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Now rename_params_rule merely issues warnings--and does nothing--if the
authorpaulson
Wed, 23 Jul 1997 11:54:32 +0200
changeset 3565 c64410e701fb
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 file | annotate | diff | comparison | revisions 
--- 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]),
isabelle