1.1 --- a/src/HOL/IsaMakefile Fri Jan 19 22:08:06 2007 +0100
1.2 +++ b/src/HOL/IsaMakefile Fri Jan 19 22:08:07 2007 +0100
1.3 @@ -482,7 +482,7 @@
1.4 Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \
1.5 Lambda/WeakNorm.thy Lambda/ROOT.ML \
1.6 Lambda/document/root.bib Lambda/document/root.tex
1.7 - @$(ISATOOL) usedir -g true $(OUT)/HOL Lambda
1.8 + @$(ISATOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
1.9
1.10
1.11 ## HOL-Prolog
2.1 --- a/src/HOL/Lambda/ROOT.ML Fri Jan 19 22:08:06 2007 +0100
2.2 +++ b/src/HOL/Lambda/ROOT.ML Fri Jan 19 22:08:07 2007 +0100
2.3 @@ -6,7 +6,6 @@
2.4
2.5 Syntax.ambiguity_level := 100;
2.6 proofs := 2;
2.7 -IsarOutput.modes := "no_brackets" :: !IsarOutput.modes;
2.8
2.9 use_thy "Eta";
2.10 no_document use_thy "Accessible_Part";