qualified name Pure.attribute;
authorwenzelm
Sat, 23 Apr 2005 19:50:23 +0200
changeset 15828 ad483e324b59
parent 15827 5fdf2d8dab9c
child 15829 652e53c4a1ed
qualified name Pure.attribute;
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 *)