src/Pure/tactic.ML
changeset 14673 3d760a971fde
parent 13925 761af5c2fd59
child 15006 107e4dfd3b96
     1.1 --- a/src/Pure/tactic.ML	Mon Apr 26 14:53:29 2004 +0200
     1.2 +++ b/src/Pure/tactic.ML	Mon Apr 26 14:54:45 2004 +0200
     1.3 @@ -566,7 +566,7 @@
     1.4  (*Calling this will generate the warning "Same as previous level" since
     1.5    it affects nothing but the names of bound variables!*)
     1.6  fun rename_params_tac xs i =
     1.7 -  case Library.find_first (not o Symbol.is_identifier) xs of
     1.8 +  case Library.find_first (not o Syntax.is_identifier) xs of
     1.9        Some x => error ("Not an identifier: " ^ x)
    1.10      | None => 
    1.11         (if !Logic.auto_rename