# HG changeset patch
# User wenzelm
# Date 1169240904 -3600
# Node ID cde511c2a625febb1fbdfa2559cb0bc51aa92579
# Parent  560c5b5dda1ccbc2c529976f0040171bbc58ed0c
removed obsolete Attribute;

diff -r 560c5b5dda1c -r cde511c2a625 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Jan 19 22:08:23 2007 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Jan 19 22:08:24 2007 +0100
@@ -8,7 +8,6 @@
 signature BASIC_ATTRIB =
 sig
   val print_attributes: theory -> unit
-  val Attribute: bstring -> (Args.src -> attribute) -> string -> unit
 end;
 
 signature ATTRIB =
@@ -138,8 +137,6 @@
         error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
   in AttributesData.map add thy end;
 
-fun Attribute name att cmt = Context.>> (add_attributes [(name, att, cmt)]);
-
 
 
 (** attribute parsers **)