src/Pure/General/markup.ML
changeset 43251 9371ea9f91fb
parent 43249 d9fe47d21b41
child 43364 83c57d850049
     1.1 --- a/src/Pure/General/markup.ML	Sun Apr 17 21:04:22 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Sun Apr 17 21:17:45 2011 +0200
     1.3 @@ -55,8 +55,6 @@
     1.4    val typN: string val typ: T
     1.5    val termN: string val term: T
     1.6    val propN: string val prop: T
     1.7 -  val attributeN: string val attribute: string -> T
     1.8 -  val methodN: string val method: string -> T
     1.9    val ML_keywordN: string val ML_keyword: T
    1.10    val ML_delimiterN: string val ML_delimiter: T
    1.11    val ML_identN: string val ML_ident: T
    1.12 @@ -237,9 +235,6 @@
    1.13  val (termN, term) = markup_elem "term";
    1.14  val (propN, prop) = markup_elem "prop";
    1.15  
    1.16 -val (attributeN, attribute) = markup_string "attribute" nameN;
    1.17 -val (methodN, method) = markup_string "method" nameN;
    1.18 -
    1.19  
    1.20  (* ML syntax *)
    1.21