# HG changeset patch
# User wenzelm
# Date 878562556 -3600
# Node ID 0ec0d2dbe3f4cbc6c6251a011dcde5bc007acd08
# Parent  71e05eb27fb6ebe75a39d40069817fd8e7fb9f76
export const_decls parser;

diff -r 71e05eb27fb6 -r 0ec0d2dbe3f4 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Nov 03 14:06:27 1997 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Mon Nov 03 14:09:16 1997 +0100
@@ -50,6 +50,7 @@
   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