# HG changeset patch
# User wenzelm
# Date 1185913282 -7200
# Node ID af364e2b40489748a05a434a116b7a0cc4a128a5
# Parent  719fbe4fb77fc9da13f7de3fefed4d3fb7172931
setmp_noncritical print_mode;

diff -r 719fbe4fb77f -r af364e2b4048 src/HOL/Unix/ROOT.ML
--- a/src/HOL/Unix/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
+++ b/src/HOL/Unix/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
@@ -1,3 +1,4 @@
+(* $Id$ *)
 
-Library.setmp print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
+setmp_noncritical print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
   use_thy "Unix";