# HG changeset patch
# User paulson
# Date 914860237 -3600
# Node ID 3eecc7fbfad869a4b54082e0cbc80f0c5e7476fc
# Parent  0ccde2f25dd65ecb880cc743aab8d7899e58ee8b
more efficient strip_quotes using "substring"

diff -r 0ccde2f25dd6 -r 3eecc7fbfad8 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Dec 28 16:50:11 1998 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Mon Dec 28 16:50:37 1998 +0100
@@ -177,8 +177,9 @@
 
 fun split_decls l = flat (map (fn (xs, y) => map (rpair y) xs) l);
 
-fun strip_quotes str =
-  implode (tl (take (size str - 1, explode str)));
+(*Remove the leading and trailing chararacters.  Actually called to
+  remove quotation marks.*)
+fun strip_quotes s = String.substring (s, 1, size s - 2);
 
 
 (* names *)