src/Pure/Syntax/syntax_trans.ML
changeset 45057 86c9b73158a8
parent 44433 9fbee4aab115
child 45389 bc0d50f8ae19
--- a/src/Pure/Syntax/syntax_trans.ML	Fri Sep 23 14:12:09 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Fri Sep 23 14:13:15 2011 +0200
@@ -12,7 +12,11 @@
 signature SYNTAX_TRANS =
 sig
   include BASIC_SYNTAX_TRANS
+  val bracketsN: string
+  val no_bracketsN: string
   val no_brackets: unit -> bool
+  val type_bracketsN: string
+  val no_type_bracketsN: string
   val no_type_brackets: unit -> bool
   val abs_tr: term list -> term
   val mk_binder_tr: string * string -> string * (term list -> term)