--- 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";