src/Pure/Isar/args.ML

--- a/src/Pure/Isar/args.ML	Wed Aug 30 16:29:21 2000 +0200
+++ b/src/Pure/Isar/args.ML	Wed Aug 30 17:53:23 2000 +0200
@@ -12,6 +12,7 @@
   val val_of: T -> string
   val pos_of: T -> Position.T
   val str_of: T -> string
+  val string_of: T -> string
   val ident: string * Position.T -> T
   val string: string * Position.T -> T
   val keyword: string * Position.T -> T
@@ -67,6 +68,11 @@
   | str_of (Arg (Keyword, (x, _))) = x
   | str_of (Arg (EOF, _)) = "end-of-text";
 
+fun string_of (Arg (Ident, (x, _))) = x
+  | string_of (Arg (String, (x, _))) = quote x
+  | string_of (Arg (Keyword, (x, _))) = x
+  | string_of (Arg (EOF, _)) = "";
+
 fun arg kind x_pos = Arg (kind, x_pos);
 val ident = arg Ident;
 val string = arg String;