--- a/src/Pure/Syntax/lexicon.ML Wed May 13 12:20:53 1998 +0200
+++ b/src/Pure/Syntax/lexicon.ML Wed May 13 12:21:45 1998 +0200
@@ -228,8 +228,9 @@
val scan_str =
$$ "'" |-- $$ "'" |--
- !! (fn cs => "Inner lexical error: malformed literal string at " ^ quote ("''" ^ beginning cs))
- (Scan.repeat scan_chr --| $$ "'" --| $$ "'");
+ !! (fn (cs, _) => "Inner lexical error: malformed literal string at " ^
+ quote ("''" ^ beginning cs))
+ (Scan.repeat scan_chr --| $$ "'" --| $$ "'");
fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));