# HG changeset patch
# User wenzelm
# Date 967650803 -7200
# Node ID 67486cf2f8f6e16b4bfaaa2edd8251d09865594a
# Parent  043098ba5098c4b7a2fa12799b919ca44f5a873b
added string_of;

diff -r 043098ba5098 -r 67486cf2f8f6 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;