more informative Token.Name with history of morphisms;
tuned signature;

--- a/src/Pure/Isar/args.ML	Thu Aug 14 19:55:00 2014 +0200
+++ b/src/Pure/Isar/args.ML	Fri Aug 15 18:02:34 2014 +0200
@@ -43,12 +43,11 @@
   val symbol: string parser
   val liberal_name: string parser
   val var: indexname parser
-  val internal_text: string parser
+  val internal_name: (string * morphism) parser
   val internal_typ: typ parser
   val internal_term: term parser
   val internal_fact: thm list parser
   val internal_attribute: (morphism -> attribute) parser
-  val named_text: (string -> string) -> string parser
   val named_typ: (string -> typ) -> typ parser
   val named_term: (string -> term) -> term parser
   val named_fact: (string -> string option * thm list) -> thm list parser
@@ -97,17 +96,7 @@
       (case output_info of
         NONE => Pretty.str name
       | SOME (_, markup) => Pretty.mark_str (markup, name));
-    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
-    fun prt_arg arg =
-      (case Token.get_value arg of
-        SOME (Token.Literal markup) =>
-          let val x = Token.content_of arg
-          in Pretty.mark_str (Token.keyword_markup markup x, x) end
-      | SOME (Token.Text s) => Pretty.str (quote s)
-      | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
-      | SOME (Token.Term t) => Syntax.pretty_term ctxt t
-      | SOME (Token.Fact (_, ths)) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
-      | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
+    val prt_arg = Token.pretty_value ctxt;
   in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
 
 
@@ -127,12 +116,7 @@
 fun map_args f (Src {name, args, output_info}) =
   Src {name = name, args = map f args, output_info = output_info};
 
-fun transform_values phi = map_args (Token.map_value
-  (fn Token.Typ T => Token.Typ (Morphism.typ phi T)
-    | Token.Term t => Token.Term (Morphism.term phi t)
-    | Token.Fact (a, ths) => Token.Fact (a, Morphism.fact phi ths)
-    | Token.Attribute att => Token.Attribute (Morphism.transform phi att)
-    | tok => tok));
+val transform_values = map_args o Token.transform_value;
 
 val init_assignable = map_args Token.init_assignable;
 val closure = map_args Token.closure;
@@ -209,13 +193,12 @@
 fun evaluate mk eval arg =
   let val x = eval arg in (Token.assign (SOME (mk x)) arg; x) end;
 
-val internal_text = value (fn Token.Text s => s);
+val internal_name = value (fn Token.Name a => a);
 val internal_typ = value (fn Token.Typ T => T);
 val internal_term = value (fn Token.Term t => t);
 val internal_fact = value (fn Token.Fact (_, ths) => ths);
 val internal_attribute = value (fn Token.Attribute att => att);
 
-fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
 fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.inner_syntax_of);
 fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
 
@@ -267,7 +250,7 @@
 fun attribs check =
   let
     fun intern tok = check (Token.content_of tok, Token.pos_of tok);
-    val attrib_name = internal_text || (symbolic || named) >> evaluate Token.Text intern;
+    val attrib_name = internal_name >> #1 || (symbolic || named) >> evaluate Token.name0 intern;
     val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry src;
   in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
 

--- a/src/Pure/Isar/token.ML	Thu Aug 14 19:55:00 2014 +0200
+++ b/src/Pure/Isar/token.ML	Fri Aug 15 18:02:34 2014 +0200
@@ -12,9 +12,14 @@
     Error of string | Sync | EOF
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   datatype value =
-    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term |
+    Literal of bool * Markup.T |
+    Name of string * morphism |
+    Typ of typ |
+    Term of term |
     Fact of string option * thm list |
-    Attribute of morphism -> attribute | Files of file Exn.result list
+    Attribute of morphism -> attribute |
+    Files of file Exn.result list
+  val name0: string -> value
   type T
   val str_of_kind: kind -> string
   val pos_of: T -> Position.T
@@ -49,17 +54,19 @@
   val markup: T -> Markup.T
   val unparse: T -> string
   val print: T -> string
+  val pretty_value: Proof.context -> T -> Pretty.T
   val text_of: T -> string * string
   val get_files: T -> file Exn.result list
   val put_files: file Exn.result list -> T -> T
   val get_value: T -> value option
   val map_value: (value -> value) -> T -> T
   val reports_of_value: T -> Position.report list
-  val mk_text: string -> T
+  val mk_name: string -> T
   val mk_typ: typ -> T
   val mk_term: term -> T
   val mk_fact: string option * thm list -> T
   val mk_attribute: (morphism -> attribute) -> T
+  val transform_value: morphism -> T -> T
   val init_assignable: T -> T
   val assign: value option -> T -> unit
   val closure: T -> T
@@ -89,13 +96,15 @@
 
 datatype value =
   Literal of bool * Markup.T |
-  Text of string |
+  Name of string * morphism |
   Typ of typ |
   Term of term |
   Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
   Attribute of morphism -> attribute |
   Files of file Exn.result list;
 
+fun name0 a = Name (a, Morphism.identity);
+
 datatype slot =
   Slot |
   Value of value option |
@@ -341,17 +350,46 @@
   | _ => []);
 
 
+(* pretty value *)
+
+fun pretty_value ctxt tok =
+  (case get_value tok of
+    SOME (Literal markup) =>
+      let val x = content_of tok
+      in Pretty.mark_str (keyword_markup markup x, x) end
+  | SOME (Name (a, _)) => Pretty.str (quote a)
+  | SOME (Typ T) => Syntax.pretty_typ ctxt T
+  | SOME (Term t) => Syntax.pretty_term ctxt t
+  | SOME (Fact (_, ths)) =>
+      Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
+  | _ => Pretty.mark_str (markup tok, unparse tok));
+
+
 (* make values *)
 
 fun mk_value k v = Token ((k, Position.no_range), (InternalValue, k), Value (SOME v));
 
-val mk_text = mk_value "<text>" o Text;
+val mk_name = mk_value "<name>" o name0;
 val mk_typ = mk_value "<typ>" o Typ;
 val mk_term = mk_value "<term>" o Term;
 val mk_fact = mk_value "<fact>" o Fact;
 val mk_attribute = mk_value "<attribute>" o Attribute;
 
 
+(* transform value *)
+
+fun transform_value phi =
+  map_value (fn v =>
+    (case v of
+      Literal _ => v
+    | Name (a, psi) => Name (a, psi $> phi)
+    | Typ T => Typ (Morphism.typ phi T)
+    | Term t => Term (Morphism.term phi t)
+    | Fact (a, ths) => Fact (a, Morphism.fact phi ths)
+    | Attribute att => Attribute (Morphism.transform phi att)
+    | Files _ => v));
+
+
 (* static binding *)
 
 (*1st stage: initialize assignable slots*)