src/Pure/Isar/attrib.ML
changeset 53044 be27b6be8027
parent 52709 0e4bacf21e77
child 53168 d998de7f0efc
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Aug 16 21:33:36 2013 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Aug 16 22:39:31 2013 +0200
     1.3 @@ -11,10 +11,10 @@
     1.4    val empty_binding: binding
     1.5    val is_empty_binding: binding -> bool
     1.6    val print_attributes: theory -> unit
     1.7 +  val check: theory -> xstring * Position.T -> string
     1.8    val intern: theory -> xstring -> string
     1.9    val intern_src: theory -> src -> src
    1.10    val pretty_attribs: Proof.context -> src list -> Pretty.T list
    1.11 -  val defined: theory -> string -> bool
    1.12    val attribute: Proof.context -> src -> attribute
    1.13    val attribute_global: theory -> src -> attribute
    1.14    val attribute_cmd: Proof.context -> src -> attribute
    1.15 @@ -114,6 +114,8 @@
    1.16  
    1.17  (* name space *)
    1.18  
    1.19 +fun check thy = #1 o Name_Space.check (Context.Theory thy) (Attributes.get thy);
    1.20 +
    1.21  val intern = Name_Space.intern o #1 o Attributes.get;
    1.22  val intern_src = Args.map_name o intern;
    1.23  
    1.24 @@ -129,8 +131,6 @@
    1.25  
    1.26  (* get attributes *)
    1.27  
    1.28 -val defined = Symtab.defined o #2 o Attributes.get;
    1.29 -
    1.30  fun attribute_generic context =
    1.31    let
    1.32      val thy = Context.theory_of context;