src/Pure/Isar/attrib.ML

--- a/src/Pure/Isar/attrib.ML	Fri Aug 16 21:33:36 2013 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Aug 16 22:39:31 2013 +0200
@@ -11,10 +11,10 @@
   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
@@ -114,6 +114,8 @@
 
 (* 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;
 
@@ -129,8 +131,6 @@
 
 (* get attributes *)
 
-val defined = Symtab.defined o #2 o Attributes.get;
-
 fun attribute_generic context =
   let
     val thy = Context.theory_of context;