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