# HG changeset patch
# User wenzelm
# Date 898366702 -7200
# Node ID 52a78ff5599e423a18fafd72fdd72036d11e79e0
# Parent  16e3fadd759ec13a6dcf340861939b4a184a290e
export mk_triple1/2;

diff -r 16e3fadd759e -r 52a78ff5599e src/Pure/Thy/thy_parse.ML
--- 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;