src/Pure/Thy/thy_parse.ML
changeset 6043 3eecc7fbfad8
parent 6022 259e4f2114e1
child 6090 78c068b838ff
equal deleted inserted replaced
6042:0ccde2f25dd6 6043:3eecc7fbfad8
   175 fun mk_triple1 ((x, y), z) = mk_triple (x, y, z);
   175 fun mk_triple1 ((x, y), z) = mk_triple (x, y, z);
   176 fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
   176 fun mk_triple2 (x, (y, z)) = mk_triple (x, y, z);
   177 
   177 
   178 fun split_decls l = flat (map (fn (xs, y) => map (rpair y) xs) l);
   178 fun split_decls l = flat (map (fn (xs, y) => map (rpair y) xs) l);
   179 
   179 
   180 fun strip_quotes str =
   180 (*Remove the leading and trailing chararacters.  Actually called to
   181   implode (tl (take (size str - 1, explode str)));
   181   remove quotation marks.*)
       
   182 fun strip_quotes s = String.substring (s, 1, size s - 2);
   182 
   183 
   183 
   184 
   184 (* names *)
   185 (* names *)
   185 
   186 
   186 val name = ident >> quote || string;
   187 val name = ident >> quote || string;