# HG changeset patch
# User wenzelm
# Date 1283772131 -7200
# Node ID b4f18ac786facb60b75f49e0ae987f7263ec4838
# Parent  3e94ebe282f1075bae869c12fe6f810576ba3564
modernized session ROOT setup;

diff -r 3e94ebe282f1 -r b4f18ac786fa src/HOL/Import/HOL/ROOT.ML
--- a/src/HOL/Import/HOL/ROOT.ML	Mon Sep 06 13:06:27 2010 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML	Mon Sep 06 13:22:11 2010 +0200
@@ -1,4 +1,2 @@
-
 use_thy "~~/src/HOL/Old_Number_Theory/Primes";
-setmp_noncritical quick_and_dirty true use_thy "HOL4Prob";
-setmp_noncritical quick_and_dirty true use_thy "HOL4";
+setmp_noncritical quick_and_dirty true use_thys ["HOL4Prob", "HOL4"];
diff -r 3e94ebe282f1 -r b4f18ac786fa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Sep 06 13:06:27 2010 +0200
+++ b/src/HOL/IsaMakefile	Mon Sep 06 13:22:11 2010 +0200
@@ -785,7 +785,7 @@
 $(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy		\
   Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy			\
   Unix/document/root.bib Unix/document/root.tex
-	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix
+	@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix
 
 
 ## HOL-ZF
diff -r 3e94ebe282f1 -r b4f18ac786fa src/HOL/Unix/ROOT.ML
--- a/src/HOL/Unix/ROOT.ML	Mon Sep 06 13:06:27 2010 +0200
+++ b/src/HOL/Unix/ROOT.ML	Mon Sep 06 13:22:11 2010 +0200
@@ -1,2 +1,1 @@
-setmp_noncritical print_mode (! print_mode @ ["no_brackets", "no_type_brackets"])
-  use_thys ["Unix"];
+use_thys ["Unix"];