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  

     2.1 --- a/src/Pure/Isar/attrib.ML	Sun Apr 17 21:04:22 2011 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Sun Apr 17 21:17:45 2011 +0200
     2.3 @@ -109,12 +109,12 @@
     2.4  
     2.5  fun attribute_i thy =
     2.6    let
     2.7 -    val attrs = #2 (Attributes.get thy);
     2.8 +    val (space, tab) = Attributes.get thy;
     2.9      fun attr src =
    2.10        let val ((name, _), pos) = Args.dest_src src in
    2.11 -        (case Symtab.lookup attrs name of
    2.12 +        (case Symtab.lookup tab name of
    2.13            NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
    2.14 -        | SOME (att, _) => (Position.report pos (Markup.attribute name); att src))
    2.15 +        | SOME (att, _) => (Position.report pos (Name_Space.markup space name); att src))
    2.16        end;
    2.17    in attr end;
    2.18  

     3.1 --- a/src/Pure/Isar/method.ML	Sun Apr 17 21:04:22 2011 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Sun Apr 17 21:17:45 2011 +0200
     3.3 @@ -356,12 +356,12 @@
     3.4  
     3.5  fun method_i thy =
     3.6    let
     3.7 -    val meths = #2 (Methods.get thy);
     3.8 +    val (space, tab) = Methods.get thy;
     3.9      fun meth src =
    3.10        let val ((name, _), pos) = Args.dest_src src in
    3.11 -        (case Symtab.lookup meths name of
    3.12 +        (case Symtab.lookup tab name of
    3.13            NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
    3.14 -        | SOME (mth, _) => (Position.report pos (Markup.method name); mth src))
    3.15 +        | SOME (mth, _) => (Position.report pos (Name_Space.markup space name); mth src))
    3.16        end;
    3.17    in meth end;
    3.18  

     4.1 --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 17 21:04:22 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sun Apr 17 21:17:45 2011 +0200
     4.3 @@ -173,8 +173,6 @@
     4.4        Markup.TYP -> NULL,
     4.5        Markup.TERM -> NULL,
     4.6        Markup.PROP -> NULL,
     4.7 -      Markup.ATTRIBUTE -> NULL,
     4.8 -      Markup.METHOD -> NULL,
     4.9        // ML syntax
    4.10        Markup.ML_KEYWORD -> KEYWORD1,
    4.11        Markup.ML_DELIMITER -> OPERATOR,