src/Pure/library.ML

--- a/src/Pure/library.ML	Wed May 12 16:54:31 1999 +0200
+++ b/src/Pure/library.ML	Wed May 12 17:26:56 1999 +0200
@@ -127,6 +127,7 @@
   val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a
   val exists_string: (string -> bool) -> string -> bool
   val enclose: string -> string -> string -> string
+  val unenclose: string -> string
   val quote: string -> string
   val space_implode: string -> string list -> string
   val commas: string list -> string
@@ -673,6 +674,7 @@
 
 (*enclose in brackets*)
 fun enclose lpar rpar str = lpar ^ str ^ rpar;
+fun unenclose str = String.substring (str, 1, size str - 2);
 
 (*simple quoting (does not escape special chars)*)
 val quote = enclose "\"" "\"";