src/Pure/tactic.ML

--- a/src/Pure/tactic.ML	Mon Nov 26 21:10:42 2012 +0100
+++ b/src/Pure/tactic.ML	Mon Nov 26 21:46:04 2012 +0100
@@ -306,7 +306,7 @@
 
 (*Renaming of parameters in a subgoal*)
 fun rename_tac xs i =
-  case Library.find_first (not o Lexicon.is_identifier) xs of
+  case Library.find_first (not o Symbol_Pos.is_identifier) xs of
       SOME x => error ("Not an identifier: " ^ x)
     | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i));