# HG changeset patch
# User wenzelm
# Date 1113410919 -7200
# Node ID 3285d665c89165c65cbea931323b7ece93371412
# Parent  f088c10208c0ed1adef5d49df68e8de8da1244c0
*** 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;

diff -r f088c10208c0 -r 3285d665c891 src/Pure/Isar/attrib.ML
--- 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;
+