src/Pure/Thy/thy_parse.ML

   val sort: token list -> string * token list
   val typ: token list -> string * token list
   val opt_infix: token list -> string * token list
   val opt_mixfix: token list -> string * token list
   val opt_witness: token list -> string * token list
+  val const_decls: token list -> string * token list
   type syntax
   val make_syntax: string list ->
     (string * (token list -> (string * string) * token list)) list -> syntax
   val parse_thy: syntax -> string -> string -> string
   val section: string -> string -> (token list -> string * token list)