diff -r 9c4ff93762a0 -r 74bc10921f7d src/Pure/Syntax/lexicon.ML
--- 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));