diff -r 98d35a7368bd -r fb579401dc26 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Nov 26 21:10:42 2012 +0100
+++ b/src/Pure/General/symbol.ML	Mon Nov 26 21:46:04 2012 +0100
@@ -53,7 +53,6 @@
   val is_block_ctrl: symbol -> bool
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
-  val is_ident: symbol list -> bool
   val beginning: int -> symbol list -> string
   val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source
   val explode: string -> symbol list
@@ -512,12 +511,6 @@
   |> implode;
 
 
-(* identifiers *)
-
-fun is_ident [] = false
-  | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;
-
-
 (* bump string -- treat as base 26 or base 1 numbers *)
 
 fun symbolic_end (_ :: "\\<^isub>" :: _) = true