# HG changeset patch
# User wenzelm
# Date 961970176 -7200
# Node ID bec42c975d13cdfb47a47db5d115cc0205372074
# Parent  8196955b02ec98174e0e2caf1c78534bcb09b0e0
use Library.change;

diff -r 8196955b02ec -r bec42c975d13 src/Pure/Thy/thy_info.ML
--- 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;