--- a/src/HOL/Unix/ROOT.ML Mon Sep 06 13:06:27 2010 +0200
+++ b/src/HOL/Unix/ROOT.ML Mon Sep 06 13:22:11 2010 +0200
@@ -1,2 +1,1 @@
-setmp_noncritical print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
- use_thys ["Unix"];
+use_thys ["Unix"];