src/Pure/General/symbol.ML
changeset 67522 9e712280cc37
parent 67512 166c1659ac75
child 69452 704915cf59fa
--- a/src/Pure/General/symbol.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Pure/General/symbol.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -199,7 +199,7 @@
 
 fun beginning n cs =
   let
-    val drop_blanks = #1 o take_suffix is_ascii_blank;
+    val drop_blanks = drop_suffix is_ascii_blank;
     val all_cs = drop_blanks cs;
     val dots = if length all_cs > n then " ..." else "";
   in
@@ -465,7 +465,7 @@
           then chr (ord s + 1) :: ss
           else "a" :: s :: ss;
 
-    val (ss, qs) = apfst rev (take_suffix is_quasi (Symbol.explode str));
+    val (ss, qs) = apfst rev (chop_suffix is_quasi (Symbol.explode str));
     val ss' = if symbolic_end ss then "'" :: ss else bump ss;
   in implode (rev ss' @ qs) end;