src/Pure/library.ML

--- a/src/Pure/library.ML	Wed Apr 04 00:11:12 2007 +0200
+++ b/src/Pure/library.ML	Wed Apr 04 00:11:13 2007 +0200
@@ -239,7 +239,6 @@
   val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
   val gensym: string -> string
-  val scanwords: (string -> bool) -> string list -> string list
   type stamp
   val stamp: unit -> stamp
   type serial
@@ -777,10 +776,11 @@
   let
     val tab_width = 8;
 
-    fun untab pos [] ys = rev ys 
+    fun untab pos [] ys = rev ys
       | untab pos ("\n" :: xs) ys = untab 0 xs ("\n" :: ys)
       | untab pos ("\t" :: xs) ys =
-          let val d = tab_width - (pos mod tab_width) in untab (pos + d) xs (replicate d " " @ ys) end
+          let val d = tab_width - (pos mod tab_width)
+          in untab (pos + d) xs (replicate d " " @ ys) end
       | untab pos (c :: xs) ys = untab (pos + 1) xs (c :: ys);
   in
     if not (exists (fn c => c = "\t") chs) then chs
@@ -1131,7 +1131,7 @@
 (** Freshly generated identifiers; supplied prefix MUST start with a letter **)
 local
 (*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
-fun gensym_char i = 
+fun gensym_char i =
   if i<26 then chr (ord "A" + i)
   else if i<52 then chr (ord "a" + i - 26)
   else chr (ord "0" + i - 52);
@@ -1146,18 +1146,6 @@
 end;
 
 
-(* lexical scanning *)
-
-(*scan a list of characters into "words" composed of "letters" (recognized by
-  is_let) and separated by any number of non-"letters"*)
-fun scanwords is_let cs =
-  let fun scan1 [] = []
-        | scan1 cs =
-            let val (lets, rest) = take_prefix is_let cs
-            in implode lets :: scanwords is_let rest end;
-  in scan1 (#2 (take_prefix (not o is_let) cs)) end;
-
-
 (* stamps and serial numbers *)
 
 type stamp = unit ref;