# HG changeset patch # User wenzelm # Date 1419263094 -3600 # Node ID 8cf1bad1c2e7b1a58f72c1c3941b603f38b9213d # Parent bf465f335e8550c69d8ca274ab19f3052a04ab38 obsolete; diff -r bf465f335e85 -r 8cf1bad1c2e7 src/Pure/library.ML --- a/src/Pure/library.ML Mon Dec 22 16:44:24 2014 +0100 +++ b/src/Pure/library.ML Mon Dec 22 16:44:54 2014 +0100 @@ -53,7 +53,6 @@ val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool val exists: ('a -> bool) -> 'a list -> bool val forall: ('a -> bool) -> 'a list -> bool - val setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c (*lists*) @@ -295,10 +294,7 @@ val forall = List.all; -(* flags *) - -fun setmp_CRITICAL flag value f x = - NAMED_CRITICAL "setmp" (fn () => Unsynchronized.setmp flag value f x); +(* thread data *) fun setmp_thread_data tag orig_data data f x = uninterruptible (fn restore_attributes => fn () =>