src/Pure/library.ML
changeset 62889 99c7f31615c2
parent 62551 df62e1ab7d88
child 62918 2fcbd4abc021
     1.1 --- a/src/Pure/library.ML	Wed Apr 06 14:08:57 2016 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Apr 06 16:33:33 2016 +0200
     1.3 @@ -48,7 +48,6 @@
     1.4    val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
     1.5    val exists: ('a -> bool) -> 'a list -> bool
     1.6    val forall: ('a -> bool) -> 'a list -> bool
     1.7 -  val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
     1.8  
     1.9    (*lists*)
    1.10    val single: 'a -> 'a list
    1.11 @@ -278,17 +277,6 @@
    1.12  val forall = List.all;
    1.13  
    1.14  
    1.15 -(* thread data *)
    1.16 -
    1.17 -fun setmp_thread_data tag orig_data data f x =
    1.18 -  uninterruptible (fn restore_attributes => fn () =>
    1.19 -    let
    1.20 -      val _ = Thread.setLocal (tag, data);
    1.21 -      val result = Exn.capture (restore_attributes f) x;
    1.22 -      val _ = Thread.setLocal (tag, orig_data);
    1.23 -    in Exn.release result end) ();
    1.24 -
    1.25 -
    1.26  
    1.27  (** lists **)
    1.28