adapted to new Scan.fail_with / Scan.!!;

--- 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));

--- a/src/Pure/Syntax/symbol.ML	Wed May 13 12:20:53 1998 +0200
+++ b/src/Pure/Syntax/symbol.ML	Wed May 13 12:21:45 1998 +0200
@@ -203,7 +203,7 @@
 
 val scan =
   ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
-    !! (fn cs => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
+    !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
       (Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
   Scan.one not_eof;
 

--- a/src/Pure/Thy/thy_scan.ML	Wed May 13 12:20:53 1998 +0200
+++ b/src/Pure/Thy/thy_scan.ML	Wed May 13 12:21:45 1998 +0200
@@ -66,7 +66,7 @@
 val scan_dig = Scan.one Symbol.is_digit;
 
 val scan_esc =
-  keep_line ($$ "\\") ^^ !! (fn (n, _) => lex_err n "bad escape sequence in string")
+  keep_line ($$ "\\") ^^ !! (fn ((n, _), _) => lex_err n "bad escape sequence in string")
     (keep_line ($$ "n" || $$ "t" || $$ "\"" || $$ "\\" ||
       scan_ctrl || scan_dig ^^ scan_dig ^^ scan_dig) ||
       (Scan.repeat1 scan_blank >> implode) ^^ keep_line ($$ "\\"));
@@ -78,7 +78,7 @@
 
 val scan_string =
   keep_line ($$ "\"") ^^
-  !! (fn (n, _) => lex_err n "missing quote at end of string")
+  !! (fn ((n, _), _) => lex_err n "missing quote at end of string")
     ((Scan.repeat scan_str >> implode) ^^ keep_line ($$ "\""));
 
 
@@ -91,7 +91,7 @@
 
 val scan_verbatim =
   keep_line ($$ "{" -- $$ "|") |--
-  !! (fn (n, _) => lex_err n "missing end of verbatim text")
+  !! (fn ((n, _), _) => lex_err n "missing end of verbatim text")
     ((Scan.repeat scan_verb >> implode) --| keep_line ($$ "|" -- $$ "}"));
 
 
@@ -106,7 +106,7 @@
 
 val scan_comment =
   keep_line ($$ "(" -- $$ "*") |--
-  !! (fn (n, _) => lex_err n "missing end of comment")
+  !! (fn ((n, _), _) => lex_err n "missing end of comment")
     (Scan.pass 0 (Scan.repeat scan_cmt) |-- keep_line ($$ "*" -- $$ ")") >> K "");