src/Pure/context.ML
changeset 26421 3dfb36923a56
parent 26413 003dd6155870
child 26428 5b2beca2087d
equal deleted inserted replaced
26420:57a626f64875 26421:3dfb36923a56
   524   | _ => error "Unknown context");
   524   | _ => error "Unknown context");
   525 
   525 
   526 fun set_thread_data context = Multithreading.put_data (tag, context);
   526 fun set_thread_data context = Multithreading.put_data (tag, context);
   527 fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
   527 fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
   528 
   528 
       
   529 nonfix >>;
   529 fun >> f = set_thread_data (SOME (map_theory f (the_thread_data ())));
   530 fun >> f = set_thread_data (SOME (map_theory f (the_thread_data ())));
   530 
   531 
   531 end;
   532 end;
   532 
   533 
   533 
   534