*** MESSAGE REFERS TO PREVIOUS VERSION ***
support embedded values and static binding -- via implicit assignment
to src tokens (cf. assignable/assign/closure);
renamed ident/string/keyword to mk_ident/mk_string/mk_keyword;
added mk_name, mk_typ, mk_term, mk_fact, mk_attribute;
added type value with map_values etc.;
removed name_dummy, added general 'maybe' combinator;
added global/local_tyname/const;
added pretty_src, pretty_attribs;
added thm_sel (from attrib.ML);
--- a/src/Pure/Isar/args.ML Wed Apr 13 18:51:28 2005 +0200
+++ b/src/Pure/Isar/args.ML Wed Apr 13 18:51:39 2005 +0200
@@ -399,3 +399,4 @@
[Pretty.enclose "[" "]" (Pretty.commas (map (pretty_src ctxt) srcs))];
end;
+