# HG changeset patch
# User wenzelm
# Date 980291192 -3600
# Node ID cfd85f5c6eac8e770beab83b3ea9962be2fa00be
# Parent  4882d65cc71694c2afd984cd4e56284621dc688e
no_brackets;

diff -r 4882d65cc716 -r cfd85f5c6eac 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";