src/Pure/Thy/thy_parse.ML
changeset 5058 52a78ff5599e
parent 4965 06914837e073
child 5248 6b04b9a88c21
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Sat Jun 20 19:53:05 1998 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Sat Jun 20 20:18:22 1998 +0200
     1.3 @@ -67,6 +67,8 @@
     1.4    val mk_big_list: string list -> string
     1.5    val mk_pair: string * string -> string
     1.6    val mk_triple: string * string * string -> string
     1.7 +  val mk_triple1: (string * string) * string -> string
     1.8 +  val mk_triple2: string * (string * string) -> string
     1.9    val strip_quotes: string -> string
    1.10  end;
    1.11