author wenzelm

Tue, 31 Jul 2007 22:21:22 +0200

changeset 24105 af364e2b4048

parent 24104 719fbe4fb77f

child 24106 f2965bf954dc

src/HOL/Unix/ROOT.ML file | annotate | diff | comparison | revisions
     1.1 --- a/src/HOL/Unix/ROOT.ML	Tue Jul 31 22:21:20 2007 +0200
     1.2 +++ b/src/HOL/Unix/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +(* $Id$ *)
     1.5  
     1.6 -Library.setmp print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
     1.7 +setmp_noncritical print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
     1.8    use_thy "Unix";