author | wenzelm |
Sat, 20 Jun 1998 20:18:22 +0200 | |
changeset 5058 | 52a78ff5599e |
parent 5057 | 16e3fadd759e |
child 5059 | dcdb21e53537 |
--- a/src/Pure/Thy/thy_parse.ML Sat Jun 20 19:53:05 1998 +0200 +++ b/src/Pure/Thy/thy_parse.ML Sat Jun 20 20:18:22 1998 +0200 @@ -67,6 +67,8 @@ val mk_big_list: string list -> string val mk_pair: string * string -> string val mk_triple: string * string * string -> string + val mk_triple1: (string * string) * string -> string + val mk_triple2: string * (string * string) -> string val strip_quotes: string -> string end;