# HG changeset patch
# User wenzelm
# Date 1114278623 -7200
# Node ID ad483e324b5910833a79f1070720e94757852971
# Parent  5fdf2d8dab9c71532e3e30af349b79667e2c52dd
qualified name Pure.attribute;

diff -r 5fdf2d8dab9c -r ad483e324b59 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Apr 23 19:50:15 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Apr 23 19:50:23 2005 +0200
@@ -481,16 +481,13 @@
 
 (* internal attribute *)
 
-val attributeN = "attribute";
-fun attribute att = Args.src ((attributeN, [Args.mk_attribute att]), Position.none);
+fun attribute att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none);
 
 fun attribute_global x = (syntax (Scan.lift Args.internal_attribute >> #1)) x;
 fun attribute_local x = (syntax (Scan.lift Args.internal_attribute >> #2)) x;
 
 val _ = Context.add_setup
- [PureThy.global_path,
-  add_attributes [(attributeN, (attribute_global, attribute_local), "internal attribute")],
-  PureThy.local_path];
+ [add_attributes [("attribute", (attribute_global, attribute_local), "internal attribute")]];
 
 
 (* pure_attributes *)