--- 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