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