src/Pure/Syntax/type_ext.ML

 sig
   val sort_of_term: term -> sort
   val raw_term_sorts: term -> (indexname * sort) list
   val typ_of_term: (indexname -> sort) -> term -> typ
   val term_of_typ: bool -> typ -> term
+  val no_brackets: unit -> bool
 end;
 
 signature TYPE_EXT =
 sig
   include TYPE_EXT0

 
 
 
 (** the type syntax **)
 
+(* print mode *)
+
+val bracketsN = "brackets";
+val no_bracketsN = "no_brackets";
+
+fun no_brackets () =
+  Library.find_first (equal bracketsN orf equal no_bracketsN) (! print_mode) = Some no_bracketsN;
+
+
 (* parse ast translations *)
 
 fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
   | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
 

   | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
   | tappl_ast_tr' (f, ty :: tys) =
       Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
 
 fun fun_ast_tr' (*"fun"*) asts =
-  (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
-    (dom as _ :: _ :: _, cod)
-      => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
-  | _ => raise Match);
+  if no_brackets () then raise Match
+  else
+    (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
+      (dom as _ :: _ :: _, cod)
+        => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
+    | _ => raise Match);
 
 
 (* type_ext *)
 
 val sortT = Type ("sort", []);