# 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)