no_brackets;
authorwenzelm
Wed, 24 Jan 2001 00:06:32 +0100
changeset 10969 cfd85f5c6eac
parent 10968 4882d65cc716
child 10970 7917e66505a4
no_brackets;
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";