src/Pure/library.ML
changeset 23826 463903573934
parent 23718 8ff68cb5860c
child 23860 31f5c9e43e57
     1.1 --- a/src/Pure/library.ML	Tue Jul 17 13:19:20 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Jul 17 13:19:21 2007 +0200
     1.3 @@ -217,10 +217,6 @@
     1.4    val one_of: 'a list -> 'a
     1.5    val frequency: (int * 'a) list -> 'a
     1.6  
     1.7 -  (*current directory*)
     1.8 -  val cd: string -> unit
     1.9 -  val pwd: unit -> string
    1.10 -
    1.11    (*misc*)
    1.12    val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
    1.13    val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
    1.14 @@ -1018,13 +1014,6 @@
    1.15  
    1.16  
    1.17  
    1.18 -(** current directory **)
    1.19 -
    1.20 -val cd = OS.FileSys.chDir;
    1.21 -val pwd = OS.FileSys.getDir;
    1.22 -
    1.23 -
    1.24 -
    1.25  (** misc **)
    1.26  
    1.27  fun divide_and_conquer decomp x =