# HG changeset patch
# User wenzelm
# Date 1213109006 -7200
# Node ID 38367dbccae55150c25d6f96e50f58164feb2896
# Parent  b21eec4372953c67a4afd82e0b37b6fe8cc8db92
removed obsolete read_idents;

diff -r b21eec437295 -r 38367dbccae5 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Tue Jun 10 16:43:23 2008 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Jun 10 16:43:26 2008 +0200
@@ -30,7 +30,6 @@
   val read_nat: string -> int option
   val read_int: string -> int option
   val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
-  val read_idents: string -> string list
   val fixedN: string
   val constN: string
 end;
@@ -401,19 +400,4 @@
 
 end;
 
-
-(* read_ident(s) *)
-
-fun read_idents str =
-  let
-    val blanks = Scan.many Symbol.is_blank;
-    val junk = Scan.many Symbol.is_regular;
-    val idents = Scan.repeat1 (blanks |-- (scan_id >> implode) --| blanks) -- junk;
-  in
-    (case Scan.read Symbol.stopper idents (Symbol.explode str) of
-      SOME (ids, []) => ids
-    | SOME (_, bad) => error ("Bad identifier: " ^ quote (implode bad))
-    | NONE => error ("No identifier found in: " ^ quote str))
-  end;
-
 end;