src/HOL/Unix/ROOT.ML
changeset 11704 3c50a2cd6f00
parent 10969 cfd85f5c6eac
child 24105 af364e2b4048
     1.1 --- a/src/HOL/Unix/ROOT.ML	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/Unix/ROOT.ML	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -1,3 +1,3 @@
     1.4  
     1.5 -Library.setmp print_mode (! print_mode @ ["no_brackets"])
     1.6 +Library.setmp print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
     1.7    use_thy "Unix";