# HG changeset patch
# User wenzelm
# Date 938795772 -7200
# Node ID b8e7fa177d62849eef9843fb1ca166c8775df887
# Parent  c092e67d12f873e66e26e406491af0f44d7256ab
added undef_global_attribute, undef_local_attribute;

diff -r c092e67d12f8 -r b8e7fa177d62 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Oct 01 10:23:13 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Oct 01 18:36:12 1999 +0200
@@ -20,6 +20,8 @@
   val global_attribute: theory -> Args.src -> theory attribute
   val local_attribute: theory -> Args.src -> Proof.context attribute
   val local_attribute': Proof.context -> Args.src -> Proof.context attribute
+  val undef_global_attribute: theory attribute
+  val undef_local_attribute: Proof.context attribute
   val add_attributes: (bstring * ((Args.src -> theory attribute) *
       (Args.src -> Proof.context attribute)) * string) list -> theory -> theory
   val global_thm: theory * Args.T list -> thm * (theory * Args.T list)
@@ -103,6 +105,12 @@
 val local_attribute = gen_attribute snd;
 val local_attribute' = local_attribute o ProofContext.theory_of;
 
+val undef_global_attribute: theory attribute =
+  fn _ => error "attribute undefined in theory context";
+
+val undef_local_attribute: Proof.context attribute =
+  fn _ => error "attribute undefined in proof context";
+
 
 (* add_attributes *)