# HG changeset patch # User wenzelm # Date 1206615986 -3600 # Node ID 3dfb36923a567c6d48d5dd8df87a9d679616436f # Parent 57a626f64875513fcce7794c0b519b94d3cea301 nonfix >>; diff -r 57a626f64875 -r 3dfb36923a56 src/Pure/context.ML --- a/src/Pure/context.ML Thu Mar 27 00:27:16 2008 +0100 +++ b/src/Pure/context.ML Thu Mar 27 12:06:26 2008 +0100 @@ -526,6 +526,7 @@ fun set_thread_data context = Multithreading.put_data (tag, context); fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context; +nonfix >>; fun >> f = set_thread_data (SOME (map_theory f (the_thread_data ()))); end;