1.1 --- a/src/HOL/Import/HOL/ROOT.ML	Mon Sep 06 13:06:27 2010 +0200
     1.2 +++ b/src/HOL/Import/HOL/ROOT.ML	Mon Sep 06 13:22:11 2010 +0200
     1.3 @@ -1,4 +1,2 @@
     1.4 -
     1.5  use_thy "~~/src/HOL/Old_Number_Theory/Primes";
     1.6 -setmp_noncritical quick_and_dirty true use_thy "HOL4Prob";
     1.7 -setmp_noncritical quick_and_dirty true use_thy "HOL4";
     1.8 +setmp_noncritical quick_and_dirty true use_thys ["HOL4Prob", "HOL4"];

     2.1 --- a/src/HOL/IsaMakefile	Mon Sep 06 13:06:27 2010 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Mon Sep 06 13:22:11 2010 +0200
     2.3 @@ -785,7 +785,7 @@
     2.4  $(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy		\
     2.5    Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy			\
     2.6    Unix/document/root.bib Unix/document/root.tex
     2.7 -	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix
     2.8 +	@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix
     2.9  
    2.10  
    2.11  ## HOL-ZF

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