# HG changeset patch
# User wenzelm
# Date 784810652 -3600
# Node ID 53fef17a729a0a718bea2bd7a95c33b04ea31e45
# Parent  0d0df9b5afe34bee9f2da4cf63f9a96d73dc4117
exported 'cat';

diff -r 0d0df9b5afe3 -r 53fef17a729a src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Nov 14 10:49:39 1994 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Mon Nov 14 11:57:32 1994 +0100
@@ -58,6 +58,7 @@
   val pure_sections:
     (string * (token list -> (string * string) * token list)) list
   (*items for building strings*)
+  val cat: string -> string -> string
   val parens: string -> string
   val brackets: string -> string
   val mk_list: string list -> string