# HG changeset patch
# User wenzelm
# Date 1006286227 -3600
# Node ID 53b7962bcdb1b2ba64cbf5a5ee72c1b6ee8a0687
# Parent  c9ff220cb6c79e07bb29eef9917dbd26ce5b8d12
moved prefixes1, suffixes1 to library.ML;

diff -r c9ff220cb6c7 -r 53b7962bcdb1 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Nov 20 20:56:42 2001 +0100
+++ b/src/Pure/General/name_space.ML	Tue Nov 20 20:57:07 2001 +0100
@@ -37,16 +37,6 @@
 structure NameSpace: NAME_SPACE =
 struct
 
-
-(** utils **)
-
-fun prefixes1 [] = []
-  | prefixes1 (x :: xs) = map (cons x) ([] :: prefixes1 xs);
-
-fun suffixes1 xs = map rev (prefixes1 (rev xs));
-
-
-
 (** long identifiers **)
 
 val separator = ".";
@@ -70,8 +60,8 @@
   let
     val uname = unpack name;
     val (q, b) = split_last uname;
-    val sfxs = suffixes1 uname;
-    val pfxs = map (fn x => x @ [b]) (prefixes1 q);
+    val sfxs = Library.suffixes1 uname;
+    val pfxs = map (fn x => x @ [b]) (Library.prefixes1 q);
   in map pack (sfxs @ pfxs) end;
 
 
@@ -151,7 +141,7 @@
       | try (nm :: nms) =
           let val (full_nm, uniq) = lookup space nm
           in if full_nm = name andalso uniq then nm else try nms end
-  in try (map pack (suffixes1 (unpack name))) end;
+  in try (map pack (Library.suffixes1 (unpack name))) end;
 
 (*prune names on output by default*)
 val long_names = ref false;