# HG changeset patch
# User paulson
# Date 1031227383 -7200
# Node ID 51c3ac47d127a86d390c6b1fed6777730e8e97c3
# Parent  18acbbd4d22518167ca049f46e15a9b8b2ec6d16
added checking so that (rename_tac "x y") is rejected, since
"x y" is not an identifier

diff -r 18acbbd4d225 -r 51c3ac47d127 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Sep 03 18:49:30 2002 +0200
+++ b/src/Pure/General/symbol.ML	Thu Sep 05 14:03:03 2002 +0200
@@ -26,6 +26,7 @@
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
   val is_blank: symbol -> bool
+  val is_identifier: symbol -> bool
   val is_symbolic: symbol -> bool
   val is_printable: symbol -> bool
   val length: symbol list -> int
@@ -111,6 +112,10 @@
   size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" orelse
   is_symbolic s;
 
+fun is_identifier s =
+  case (explode s) of
+      [] => false
+    | c::cs => is_letter c andalso forall is_letdig cs;
 
 fun sym_length ss = foldl (fn (n, s) =>
   (if not (is_printable s) then 0 else
diff -r 18acbbd4d225 -r 51c3ac47d127 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Sep 03 18:49:30 2002 +0200
+++ b/src/Pure/tactic.ML	Thu Sep 05 14:03:03 2002 +0200
@@ -560,10 +560,13 @@
 (*Calling this will generate the warning "Same as previous level" since
   it affects nothing but the names of bound variables!*)
 fun rename_params_tac xs i =
-  (if !Logic.auto_rename
-    then (warning "Resetting Logic.auto_rename";
-        Logic.auto_rename := false)
-   else (); PRIMITIVE (rename_params_rule (xs, i)));
+  case Library.find_first (not o Symbol.is_identifier) xs of
+      Some x => error ("Not an identifier: " ^ x)
+    | None => 
+       (if !Logic.auto_rename
+	 then (warning "Resetting Logic.auto_rename";
+	     Logic.auto_rename := false)
+	else (); PRIMITIVE (rename_params_rule (xs, i)));
 
 fun rename_tac str i =
   let val cs = Symbol.explode str in