removed legacy |>>>
authorhaftmann
Thu Oct 09 08:47:28 2008 +0200 (2008-10-09)
changeset 285383147236326ea
parent 28537 1e84256d1a8a
child 28539 bdb308737bfd
removed legacy |>>>
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Oct 09 08:47:27 2008 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Oct 09 08:47:28 2008 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  See also General/basics.ML for the most fundamental concepts.
     1.5  *)
     1.6  
     1.7 -infix 1 |>>>
     1.8  infix 2 ?
     1.9  infix 3 o oo ooo oooo
    1.10  infix 4 ~~ upto downto
    1.11 @@ -24,7 +23,6 @@
    1.12    val K: 'a -> 'b -> 'a
    1.13    val curry: ('a * 'b -> 'c) -> 'a -> 'b -> 'c
    1.14    val uncurry: ('a -> 'b -> 'c) -> 'a * 'b -> 'c
    1.15 -  val |>>> : ('a * 'c) * ('a -> 'b * 'd) -> 'b * ('c * 'd)
    1.16    val ? : bool * ('a -> 'a) -> 'a -> 'a
    1.17    val oo: ('a -> 'b) * ('c -> 'd -> 'a) -> 'c -> 'd -> 'b
    1.18    val ooo: ('a -> 'b) * ('c -> 'd -> 'e -> 'a) -> 'c -> 'd -> 'e -> 'b
    1.19 @@ -257,9 +255,6 @@
    1.20  fun curry f x y = f (x, y);
    1.21  fun uncurry f (x, y) = f x y;
    1.22  
    1.23 -(*application and structured results -- old version*)
    1.24 -fun (x, y) |>>> f = let val (x', z) = f x in (x', (y, z)) end;
    1.25 -
    1.26  (*conditional application*)
    1.27  fun b ? f = fn x => if b then f x else x;
    1.28