src/HOL/Unix/ROOT.ML

--- a/src/HOL/Unix/ROOT.ML	Tue Jan 23 18:17:14 2001 +0100
+++ b/src/HOL/Unix/ROOT.ML	Wed Jan 24 00:06:32 2001 +0100
@@ -1,2 +1,3 @@
 
-use_thy "Unix";
+Library.setmp print_mode (! print_mode @ ["no_brackets"])
+  use_thy "Unix";