strip_quotes now exported;
authorwenzelm
Tue Oct 25 13:16:49 1994 +0100 (1994-10-25)
changeset 656ec05d2fdfeee
parent 655 9748dbcd4157
child 657 2b16819fbd71
strip_quotes now exported;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Oct 25 13:15:34 1994 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Oct 25 13:16:49 1994 +0100
     1.3 @@ -58,12 +58,13 @@
     1.4    val pure_sections:
     1.5      (string * (token list -> (string * string) * token list)) list
     1.6    (*items for building strings*)
     1.7 -  val parens: string -> string   
     1.8 -  val brackets: string -> string   
     1.9 -  val mk_list: string list -> string   
    1.10 -  val mk_big_list: string list -> string   
    1.11 -  val mk_pair: string * string -> string   
    1.12 -  val mk_triple: string * string * string -> string   
    1.13 +  val parens: string -> string
    1.14 +  val brackets: string -> string
    1.15 +  val mk_list: string list -> string
    1.16 +  val mk_big_list: string list -> string
    1.17 +  val mk_pair: string * string -> string
    1.18 +  val mk_triple: string * string * string -> string
    1.19 +  val strip_quotes: string -> string
    1.20  end;
    1.21  
    1.22  functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE =