# HG changeset patch
# User nipkow
# Date 990350441 -7200
# Node ID 4104bd8d152800d707998493c9a4bd42e7725350
# Parent  5a659c4064659fe9419b4d3830202b970704024f
added (no)_type_brackets

diff -r 5a659c406465 -r 4104bd8d1528 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Sat May 19 12:21:34 2001 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Sun May 20 11:20:41 2001 +0200
@@ -129,7 +129,16 @@
 val no_bracketsN = "no_brackets";
 
 fun no_brackets () =
-  Library.find_first (equal bracketsN orf equal no_bracketsN) (! print_mode) = Some no_bracketsN;
+  Library.find_first (equal bracketsN orf equal no_bracketsN) (! print_mode)
+  = Some no_bracketsN;
+
+val type_bracketsN = "type_brackets";
+val no_type_bracketsN = "no_type_brackets";
+
+fun no_type_brackets () =
+  Library.find_first (equal type_bracketsN orf equal no_type_bracketsN)
+                     (! print_mode)
+  = Some no_type_bracketsN;
 
 
 (* parse ast translations *)
@@ -154,7 +163,7 @@
       Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
 
 fun fun_ast_tr' (*"fun"*) asts =
-  if no_brackets () then raise Match
+  if no_brackets() orelse no_type_brackets() then raise Match
   else
     (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
       (dom as _ :: _ :: _, cod)