changeset 23642 | 10672e025b83 |
parent 23637 | f3e16ee56f32 |
child 23644 | e28b8e8a85b6 |
--- 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);