--- a/src/Pure/Isar/attrib.ML Wed May 14 14:43:38 2008 +0200
+++ b/src/Pure/Isar/attrib.ML Wed May 14 20:30:05 2008 +0200
@@ -17,6 +17,7 @@
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: theory -> src -> attribute
val attribute_i: theory -> src -> attribute
val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
@@ -93,6 +94,8 @@
(* get attributes *)
+val defined = Symtab.defined o #2 o Attributes.get;
+
fun attribute_i thy =
let
val attrs = #2 (Attributes.get thy);