diff -r 6e5de8d4290a -r 3c50a2cd6f00 src/HOL/Unix/ROOT.ML
--- a/src/HOL/Unix/ROOT.ML	Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Unix/ROOT.ML	Sat Oct 06 00:02:46 2001 +0200
@@ -1,3 +1,3 @@
 
-Library.setmp print_mode (! print_mode @ ["no_brackets"])
+Library.setmp print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
   use_thy "Unix";