more efficient strip_quotes using "substring"
authorpaulson
Mon Dec 28 16:50:37 1998 +0100 (1998-12-28)
changeset 60433eecc7fbfad8
parent 6042 0ccde2f25dd6
child 6044 e0f9d930e956
more efficient strip_quotes using "substring"
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Dec 28 16:50:11 1998 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Dec 28 16:50:37 1998 +0100
     1.3 @@ -177,8 +177,9 @@
     1.4  
     1.5  fun split_decls l = flat (map (fn (xs, y) => map (rpair y) xs) l);
     1.6  
     1.7 -fun strip_quotes str =
     1.8 -  implode (tl (take (size str - 1, explode str)));
     1.9 +(*Remove the leading and trailing chararacters.  Actually called to
    1.10 +  remove quotation marks.*)
    1.11 +fun strip_quotes s = String.substring (s, 1, size s - 2);
    1.12  
    1.13  
    1.14  (* names *)