src/Pure/tactic.ML

      separated by blanks ***)
 
 (*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
   case #2 (take_prefix (Symbol.is_letdig orf Symbol.is_blank) cs) of
       [] => rename_params_tac (scanwords Symbol.is_letdig cs) i