# HG changeset patch
# User lcp
# Date 777546460 -7200
# Node ID 6333c181a3f7200be2ec1b1b8758ff827742770a
# Parent  4dc184a3d09b427f138dd577dd81a604ec450926
Pure/Thy/thy_parse/THY_PARSE: deleted duplicate specifications of parens,
brackets, ..., mk_triple

diff -r 4dc184a3d09b -r 6333c181a3f7 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Aug 22 11:03:52 1994 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Mon Aug 22 11:07:40 1994 +0200
@@ -43,12 +43,6 @@
   val sort: token list -> string * token list
   val opt_infix: token list -> string * token list
   val opt_mixfix: token list -> string * token list
-  val parens: string -> string
-  val brackets: string -> string
-  val mk_list: string list -> string
-  val mk_big_list: string list -> string
-  val mk_pair: string * string -> string
-  val mk_triple: string * string * string -> string
   type syntax
   val make_syntax: string list ->
     (string * (token list -> (string * string) * token list)) list -> syntax
@@ -61,6 +55,13 @@
   val pure_keywords: string list
   val pure_sections:
     (string * (token list -> (string * string) * token list)) list
+  (*items for building strings*)
+  val parens	: string -> string   
+  val brackets	: string -> string   
+  val mk_list	: string list -> string   
+  val mk_big_list : string list -> string   
+  val mk_pair	: string * string -> string   
+  val mk_triple	: string * string * string -> string   
 end;
 
 functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE =
@@ -82,8 +83,8 @@
 
 fun eof_err () = error "Unexpected end-of-file";
 
-(*similar to Prolog's cut: reports any syntax error instead of
-  backtracking through a superior ||*)
+(*Similar to Prolog's cut: reports any syntax error instead of backtracking
+  through a superior || *)
 fun !! parse toks = parse toks
   handle SYNTAX_ERROR (s1, s2, n) => error ("Syntax error on line " ^
     string_of_int n ^ ": " ^ s1 ^ " expected and " ^ s2 ^ " was found");