src/Pure/Isar/attrib.ML

   type src = Args.src
   type binding = binding * src list
   val empty_binding: binding
   val is_empty_binding: binding -> bool
   val print_attributes: theory -> unit
+  val check: theory -> xstring * Position.T -> string
   val intern: theory -> xstring -> string
   val intern_src: theory -> src -> src
   val pretty_attribs: Proof.context -> src list -> Pretty.T list
-  val defined: theory -> string -> bool
   val attribute: Proof.context -> src -> attribute
   val attribute_global: theory -> src -> attribute
   val attribute_cmd: Proof.context -> src -> attribute
   val attribute_cmd_global: theory -> src -> attribute
   val map_specs: ('a list -> 'att list) ->

   |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd);
 
 
 (* name space *)
 
+fun check thy = #1 o Name_Space.check (Context.Theory thy) (Attributes.get thy);
+
 val intern = Name_Space.intern o #1 o Attributes.get;
 val intern_src = Args.map_name o intern;
 
 fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (Proof_Context.theory_of ctxt)));
 

   | pretty_attribs ctxt srcs =
       [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
 
 
 (* get attributes *)
-
-val defined = Symtab.defined o #2 o Attributes.get;
 
 fun attribute_generic context =
   let
     val thy = Context.theory_of context;
     val (space, tab) = Attributes.get thy;