src/Pure/library.ML
changeset 21962 279b129498b6
parent 21942 d6218d0f9ec3
child 22142 2b54aa7586e2
     1.1 --- a/src/Pure/library.ML	Sat Dec 30 12:41:59 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Sat Dec 30 16:08:00 2006 +0100
     1.3 @@ -75,7 +75,6 @@
     1.4    val toggle: bool ref -> bool
     1.5    val change: 'a ref -> ('a -> 'a) -> unit
     1.6    val setmp: 'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c
     1.7 -  val conditional: bool -> (unit -> unit) -> unit
     1.8  
     1.9    (*lists*)
    1.10    exception UnequalLengths
    1.11 @@ -395,11 +394,6 @@
    1.12    in release result end;
    1.13  
    1.14  
    1.15 -(* conditional execution *)
    1.16 -
    1.17 -fun conditional b f = if b then f () else ();
    1.18 -
    1.19 -
    1.20  
    1.21  (** lists **)
    1.22