1.1 --- a/src/Pure/General/markup.ML	Sat Apr 09 23:29:50 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Mon Apr 11 17:11:03 2011 +0200
     1.3 @@ -71,10 +71,9 @@
     1.4    val ML_stringN: string val ML_string: T
     1.5    val ML_commentN: string val ML_comment: T
     1.6    val ML_malformedN: string val ML_malformed: T
     1.7 -  val ML_defN: string val ML_def: T
     1.8 -  val ML_openN: string val ML_open: T
     1.9 -  val ML_structN: string val ML_struct: T
    1.10 -  val ML_refN: string val ML_ref: T
    1.11 +  val ML_defN: string
    1.12 +  val ML_openN: string
    1.13 +  val ML_structN: string
    1.14    val ML_typingN: string val ML_typing: T
    1.15    val ML_sourceN: string val ML_source: T
    1.16    val doc_sourceN: string val doc_source: T
    1.17 @@ -264,10 +263,9 @@
    1.18  val (ML_commentN, ML_comment) = markup_elem "ML_comment";
    1.19  val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
    1.20  
    1.21 -val (ML_defN, ML_def) = markup_elem "ML_def";
    1.22 -val (ML_openN, ML_open) = markup_elem "ML_open";
    1.23 -val (ML_structN, ML_struct) = markup_elem "ML_struct";
    1.24 -val (ML_refN, ML_ref) = markup_elem "ML_ref";
    1.25 +val ML_defN = "ML_def";
    1.26 +val ML_openN = "ML_open";
    1.27 +val ML_structN = "ML_struct";
    1.28  val (ML_typingN, ML_typing) = markup_elem "ML_typing";
    1.29  
    1.30