--- 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 *)