--- a/src/Pure/ML/ml_lex.ML Mon Jan 20 19:47:31 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Mon Jan 20 20:04:52 2014 +0100
@@ -137,7 +137,9 @@
open Basic_Symbol_Pos;
-fun !!! msg = Symbol_Pos.!!! (fn () => "SML lexical error: " ^ msg);
+val err_prefix = "SML lexical error: ";
+
+fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
(* blanks *)
@@ -261,7 +263,7 @@
(scan_char >> token Char ||
scan_string >> token String ||
scan_blanks1 >> token Space ||
- Symbol_Pos.scan_comment !!! >> token Comment ||
+ Symbol_Pos.scan_comment err_prefix >> token Comment ||
Scan.max token_leq
(scan_keyword >> token Keyword)
(scan_word >> token Word ||