--- a/src/HOL/IsaMakefile Fri Jan 19 22:08:06 2007 +0100
+++ b/src/HOL/IsaMakefile Fri Jan 19 22:08:07 2007 +0100
@@ -482,7 +482,7 @@
Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \
Lambda/WeakNorm.thy Lambda/ROOT.ML \
Lambda/document/root.bib Lambda/document/root.tex
- @$(ISATOOL) usedir -g true $(OUT)/HOL Lambda
+ @$(ISATOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
## HOL-Prolog
--- a/src/HOL/Lambda/ROOT.ML Fri Jan 19 22:08:06 2007 +0100
+++ b/src/HOL/Lambda/ROOT.ML Fri Jan 19 22:08:07 2007 +0100
@@ -6,7 +6,6 @@
Syntax.ambiguity_level := 100;
proofs := 2;
-IsarOutput.modes := "no_brackets" :: !IsarOutput.modes;
use_thy "Eta";
no_document use_thy "Accessible_Part";