diff -r 8b9a372b3e90 -r 515fa02eee9a src/Pure/basis.ML
--- a/src/Pure/basis.ML	Fri Jun 04 11:51:31 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,192 +0,0 @@
-(*  Title:      Pure/basis.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Basis Library emulation.  Needed for Poly/ML and Standard ML of New
-Jersey version 0.93 to 1.08.  Full compatibility cannot be obtained
-using a file: what about char constants?
-*)
-
-exception Subscript;
-
-structure Bool =
-  struct
-  fun toString true  = "true"
-    | toString false = "false"
-  end;
-
-
-structure Option =
-  struct
-  exception Option
-
-  datatype 'a option = NONE | SOME of 'a
-
-  fun getOpt (SOME v, _) = v
-    | getOpt (NONE,   a) = a
-
-  fun isSome (SOME _) = true 
-    | isSome NONE     = false
-
-  fun valOf (SOME v) = v
-    | valOf NONE     = raise Option
-  end;
-
-
-structure Int =
-  struct
-  type int = int
-  fun toString (i: int) = makestring i;
-  fun max (x, y) = if x < y then y else x : int;
-  fun min (x, y) = if x < y then x else y : int;
-  end;
-
-
-structure Real =
-  struct
-  fun toString (x: real) = makestring x;
-  fun max (x, y) = if x < y then y else x : real;
-  fun min (x, y) = if x < y then x else y : real;
-  val real = real;
-  val floor = floor;
-  fun ceil x = ~1 - floor (~ (x + 1.0));
-  fun round x = floor (x + 0.5);  (*does not do round-to-nearest*)
-  fun trunc x = if x < 0.0 then ceil x else floor x;
-  end;
-
-
-structure List =
-  struct
-  exception Empty
-
-  fun last []      = raise Empty
-    | last [x]     = x
-    | last (x::xs) = last xs;
-
-  fun nth (xs, n) =
-      let fun h []      _ = raise Subscript
-	    | h (x::xs) n = if n=0 then x else h xs (n-1)
-      in if n<0 then raise Subscript else h xs n end;
-
-  fun drop (xs, n) =
-      let fun h xs      0 = xs
-	    | h []      n = raise Subscript
-	    | h (x::xs) n = h xs (n-1)
-      in if n<0 then raise Subscript else h xs n end;
-
-  fun take (xs, n) =
-      let fun h xs      0 = []
-	    | h []      n = raise Subscript
-	    | h (x::xs) n = x :: h xs (n-1)
-      in if n<0 then raise Subscript else h xs n end;
-
-  fun concat []      = []
-    | concat (l::ls) = l @ concat ls;
-
-  fun mapPartial f []      = []
-    | mapPartial f (x::xs) = 
-         (case f x of Option.NONE   => mapPartial f xs
-                    | Option.SOME y => y :: mapPartial f xs);
-
-  fun find _ []        = Option.NONE
-    | find p (x :: xs) = if p x then Option.SOME x else find p xs;
-
-
-  (*copy the list preserving elements that satisfy the predicate*)
-  fun filter p [] = []
-    | filter p (x :: xs) = if p x then x :: filter p xs else filter p xs;
-
-  (*Partition list into elements that satisfy predicate and those that don't.
-    Preserves order of elements in both lists.*)
-  fun partition (p: 'a->bool) (ys: 'a list) : ('a list * 'a list) =
-      let fun part ([], answer) = answer
-	    | part (x::xs, (ys, ns)) = if p(x)
-	      then  part (xs, (x::ys, ns))
-	      else  part (xs, (ys, x::ns))
-      in  part (rev ys, ([], []))  end;
-
-  end;
-
-
-structure ListPair =
-  struct
-  fun zip ([], [])      = []
-    | zip (x::xs,y::ys) = (x,y) :: zip(xs,ys);
-
-  fun unzip [] = ([],[])
-    | unzip((x,y)::pairs) =
-	  let val (xs,ys) = unzip pairs
-	  in  (x::xs, y::ys)  end;
-
-  fun map f ([], [])      = []
-    | map f (x::xs,y::ys) = f(x,y) :: map f (xs,ys);
-
-  fun exists p =
-    let fun boolf ([], [])      = false
-	  | boolf (x::xs,y::ys) = p(x,y) orelse boolf (xs,ys)
-    in boolf end;
-
-  fun all p =
-    let fun boolf ([], [])      = true
-	  | boolf (x::xs,y::ys) = p(x,y) andalso boolf (xs,ys)
-    in boolf end;
-  end;
-
-
-structure TextIO =
-  struct
-  type instream = instream
-  and  outstream = outstream
-  exception Io of {name: string, function: string, cause: exn}
-  val stdIn 	= std_in
-  val stdOut 	= std_out
-  val stdErr 	= std_out
-  val openIn 	= open_in
-  val openAppend = open_append
-  val openOut 	= open_out
-  val closeIn 	= close_in
-  val closeOut 	= close_out
-  val inputN 	= input
-  val inputAll  = fn is => inputN (is, 999999)
-  val inputLine = input_line
-  val endOfStream = end_of_stream
-  val output 	= output
-  val flushOut 	= flush_out
-  end;
-
-
-fun print s = (output (std_out, s); flush_out std_out);
-
-
-structure General =
-struct
-
-local
-  fun raised name = "exception " ^ name ^ " raised";
-  fun raised_msg name msg = raised name ^ ": " ^ msg;
-in
-  fun exnMessage Match = raised_msg "Match" "nonexhaustive match failure"
-    | exnMessage Bind = raised_msg "Bind" "nonexhaustive binding failure"
-    | exnMessage (Io msg) = "I/O error: " ^ msg
-    | exnMessage Neg = raised "Neg"
-    | exnMessage Sum = raised "Sum"
-    | exnMessage Diff = raised "Diff"
-    | exnMessage Prod = raised "Prod"
-    | exnMessage Quot = raised "Quot"
-    | exnMessage Abs = raised "Abs"
-    | exnMessage Div = raised "Div"
-    | exnMessage Mod = raised "Mod"
-    | exnMessage Floor = raised "Floor"
-    | exnMessage Sqrt = raised "Sqrt"
-    | exnMessage Exp = raised "Exp"
-    | exnMessage Ln = raised "Ln"
-    | exnMessage Ord = raised "Ord"
-    | exnMessage Subscript = raised_msg "Subscript " "subscript out of bounds"
-    | exnMessage Option.Option = raised "Option.Option"
-    | exnMessage List.Empty = raised "List.Empty"
-    | exnMessage (TextIO.Io {name, ...}) = raised_msg "TextIO.Io" name
-    | exnMessage exn = raised "???";
-end;
-
-end;