# HG changeset patch
# User wenzelm
# Date 1210789805 -7200
# Node ID bfa1944e523891f7910ef8ea04e3232458c48147
# Parent  f9ec18f7c0f6bcfd40b81de0cb958b9e903ffbc8
added defined;

diff -r f9ec18f7c0f6 -r bfa1944e5238 src/Pure/Isar/attrib.ML
--- 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);