diff -r d5d5ad4b78c5 -r 1095d2213b9d src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Fri Oct 28 22:28:06 2005 +0200
+++ b/src/Pure/Isar/args.ML	Fri Oct 28 22:28:07 2005 +0200
@@ -14,6 +14,7 @@
   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
@@ -46,6 +47,7 @@
   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
@@ -102,7 +104,7 @@
   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;
 
@@ -121,7 +123,8 @@
 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, _, _), _)) = "";
 
@@ -136,6 +139,7 @@
 
 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;
@@ -227,6 +231,9 @@
 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));
 
@@ -251,6 +258,7 @@
 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;
 
@@ -289,7 +297,7 @@
 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 *)