# HG changeset patch
# User wenzelm
# Date 1169240887 -3600
# Node ID 33d7468302bb86a4daf696cdeeb1c62b527909a1
# Parent  5dc00ac4bd8e660a1a26ca2185af471993c9bf6c
HOL-Lambda: usedir -m no_brackets;

diff -r 5dc00ac4bd8e -r 33d7468302bb src/HOL/IsaMakefile
--- 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
diff -r 5dc00ac4bd8e -r 33d7468302bb src/HOL/Lambda/ROOT.ML
--- 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";