src/Pure/library.ML
changeset 21479 63e7eb863ae6
parent 21395 f34ac19659ae
child 21565 bd28361f4c5b
     1.1 --- a/src/Pure/library.ML	Thu Nov 23 00:52:03 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Nov 23 00:52:07 2006 +0100
     1.3 @@ -62,7 +62,6 @@
     1.4    val apfst: ('a -> 'b) -> 'a * 'c -> 'b * 'c
     1.5    val apsnd: ('a -> 'b) -> 'c * 'a -> 'c * 'b
     1.6    val pairself: ('a -> 'b) -> 'a * 'a -> 'b * 'b
     1.7 -  val string_of_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
     1.8  
     1.9    (*booleans*)
    1.10    val equal: ''a -> ''a -> bool
    1.11 @@ -164,8 +163,6 @@
    1.12    val unsuffix: string -> string -> string
    1.13    val replicate_string: int -> string -> string
    1.14    val translate_string: (string -> string) -> string -> string
    1.15 -  val string_of_list: ('a -> string) -> 'a list -> string
    1.16 -  val string_of_option: ('a -> string) -> 'a option -> string
    1.17  
    1.18    (*lists as sets -- see also Pure/General/ord_list.ML*)
    1.19    val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
    1.20 @@ -355,8 +352,6 @@
    1.21  fun apsnd f (x, y) = (x, f y);
    1.22  fun pairself f (x, y) = (f x, f y);
    1.23  
    1.24 -fun string_of_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
    1.25 -
    1.26  
    1.27  (* booleans *)
    1.28  
    1.29 @@ -549,8 +544,7 @@
    1.30    | unflat [] [] = []
    1.31    | unflat _ _ = raise UnequalLengths;
    1.32  
    1.33 -fun burrow f xss =
    1.34 -  unflat xss ((f o flat) xss);
    1.35 +fun burrow f xss = unflat xss (f (flat xss));
    1.36  
    1.37  fun fold_burrow f xss s =
    1.38    apfst (unflat xss) (f (flat xss) s);
    1.39 @@ -819,11 +813,6 @@
    1.40        if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
    1.41        else replicate_string (k div 2) (a ^ a) ^ a;
    1.42  
    1.43 -fun string_of_list f = enclose "[" "]" o commas o map f;
    1.44 -
    1.45 -fun string_of_option f NONE = "NONE"
    1.46 -  | string_of_option f (SOME x) = "SOME (" ^ f x ^ ")";
    1.47 -
    1.48  
    1.49  
    1.50  (** lists as sets -- see also Pure/General/ord_list.ML **)