*** MESSAGE REFERS TO PREVIOUS VERSION ***
type src = Args.src;
renamed local_attribute' to context_attribute;
added _i versions of global/local/context_attribute and separate intern/intern_src;
added crude_closure to produce argument closure without knowing facts in advance;
added 'attribute' to embed internal attributes into src;
removed multi_attribute etc.;
moved thm_sel to args.ML;
Scan.peek;
read_instantiate/'where'/'of': support arbitrary mix of external /
internal typ / term args, with proper treatment of static binding;

--- a/src/Pure/Isar/attrib.ML	Wed Apr 13 18:48:19 2005 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed Apr 13 18:48:39 2005 +0200
@@ -531,3 +531,4 @@
 
 structure BasicAttrib: BASIC_ATTRIB = Attrib;
 open BasicAttrib;
+