# HG changeset patch
# User wenzelm
# Date 1183826867 -7200
# Node ID 10672e025b83a1a380a00a1a69a2ed59e6c09e9e
# Parent  d6f9d3acffaa66df43ca8b638cda6a5ddd06aec7
make smlnj happy;

diff -r d6f9d3acffaa -r 10672e025b83 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Jul 07 18:39:21 2007 +0200
+++ b/src/Pure/General/markup.ML	Sat Jul 07 18:47:47 2007 +0200
@@ -46,7 +46,7 @@
 
 val none = ("", []);
 
-fun markup kind = (kind, (kind, []));
+fun markup kind = (kind, (kind, []): T);
 fun markup_name kind = (kind, fn name => (kind, [(nameN, name)]): T);