# HG changeset patch
# User wenzelm
# Date 783087409 -3600
# Node ID ec05d2fdfeeeae280e05320a58163c00ea8dda41
# Parent  9748dbcd4157692ab50f6622412fdd9c4ba5fd36
strip_quotes now exported;

diff -r 9748dbcd4157 -r ec05d2fdfeee src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Tue Oct 25 13:15:34 1994 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Tue Oct 25 13:16:49 1994 +0100
@@ -58,12 +58,13 @@
   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   
+  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
+  val strip_quotes: string -> string
 end;
 
 functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE =