changeset 14673 | 3d760a971fde |
parent 13925 | 761af5c2fd59 |
child 15006 | 107e4dfd3b96 |
--- a/src/Pure/tactic.ML Mon Apr 26 14:53:29 2004 +0200 +++ b/src/Pure/tactic.ML Mon Apr 26 14:54:45 2004 +0200 @@ -566,7 +566,7 @@ (*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 = - case Library.find_first (not o Symbol.is_identifier) xs of + case Library.find_first (not o Syntax.is_identifier) xs of Some x => error ("Not an identifier: " ^ x) | None => (if !Logic.auto_rename