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