use Library.change;

--- a/src/Pure/Thy/thy_info.ML	Sun Jun 25 23:55:58 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Jun 25 23:56:16 2000 +0200
@@ -113,7 +113,7 @@
   val database = ref (Graph.empty: thy Graph.T);
 in
   fun get_thys () = ! database;
-  fun change_thys f = database := (f (! database));
+  val change_thys = Library.change database;
 end;