src/Pure/Isar/args.ML

     Attribute of theory attribute * ProofContext.context attribute
   type T
   val string_of: T -> string
   val mk_ident: string * Position.T -> T
   val mk_string: string * Position.T -> T
+  val mk_alt_string: string * Position.T -> T
   val mk_keyword: string * Position.T -> T
   val mk_name: string -> T
   val mk_typ: typ -> T
   val mk_term: term -> T
   val mk_fact: thm list -> T

   val parens: (T list -> 'a * T list) -> T list -> 'a * T list
   val bracks: (T list -> 'a * T list) -> T list -> 'a * T list
   val mode: string -> 'a * T list -> bool * ('a * T list)
   val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
   val name: T list -> string * T list
+  val alt_name: T list -> string * T list
   val symbol: T list -> string * T list
   val liberal_name: T list -> string * T list
   val nat: T list -> int * T list
   val int: T list -> int * T list
   val var: T list -> indexname * T list

 (*An argument token is a symbol (with raw string value), together with
   an optional assigned internal value.  Note that an assignable ref
   designates an intermediate state of internalization -- it is NOT
   meant to persist.*)
 
-datatype kind = Ident | String | Keyword | EOF;
+datatype kind = Ident | String | AltString | Keyword | EOF;
 
 type symbol = kind * string * Position.T;
 
 datatype value =
   Name of string |

   Assignable of value option ref;
 
 datatype T = Arg of symbol * slot;
 
 fun string_of (Arg ((Ident, x, _), _)) = x
-  | string_of (Arg ((String, x, _), _)) = Library.quote x
+  | string_of (Arg ((String, x, _), _)) = quote x
+  | string_of (Arg ((AltString, x, _), _)) = enclose "`" "`" x
   | string_of (Arg ((Keyword, x, _), _)) = x
   | string_of (Arg ((EOF, _, _), _)) = "";
 
 fun sym_of (Arg ((_, x, _), _)) = x;
 fun pos_of (Arg ((_, _, pos), _)) = pos;

 fun mk_symbol k (x, p) = Arg ((k, x, p), Empty);
 fun mk_value k v = Arg ((Keyword, k, Position.none), Value (SOME v));
 
 val mk_ident = mk_symbol Ident;
 val mk_string = mk_symbol String;
+val mk_alt_string = mk_symbol AltString;
 val mk_keyword = mk_symbol Keyword;
 val mk_name = mk_value "<name>" o Name;
 val mk_typ = mk_value "<typ>" o Typ;
 val mk_term = mk_value "<term>" o Term;
 val mk_fact = mk_value "<fact>" o Fact;

 fun some_ident f =
   touch (Scan.some (fn Arg ((Ident, x, _), _) => f x | _ => NONE));
 
 val named =
   touch (Scan.one (fn Arg ((k, _, _), _) => k = Ident orelse k = String));
+
+val alt_string =
+  touch (Scan.one (fn Arg ((k, _, _), _) => k = AltString));
 
 val symbolic =
   touch (Scan.one (fn Arg ((k, x, _), _) => k = Keyword andalso OuterLex.is_sid x));
 
 fun &&& x =

 fun bracks scan = $$$ "[" |-- scan --| $$$ "]";
 fun mode s = Scan.lift (Scan.optional (parens ($$$ s) >> K true) false);
 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
 
 val name = named >> sym_of;
+val alt_name = alt_string >> sym_of;
 val symbol = symbolic >> sym_of;
 val liberal_name = symbol || name;
 
 val nat = some_ident Syntax.read_nat;
 val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;

 val internal_attribute = value (fn Attribute att => att);
 
 fun named_name intern = internal_name || named >> evaluate Name intern;
 fun named_typ readT = internal_typ || named >> evaluate Typ readT;
 fun named_term read = internal_term || named >> evaluate Term read;
-fun named_fact get = internal_fact || named >> evaluate Fact get;
+fun named_fact get = internal_fact || (alt_string || named) >> evaluate Fact get;
 
 
 (* terms and types *)
 
 val global_typ_abbrev = Scan.peek (named_typ o ProofContext.read_typ_abbrev o ProofContext.init);